Theorem elab2 3348

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)

Hypotheses

Ref	Expression
elab2.1	⊢ 𝐴 ∈ V
elab2.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
elab2.3	⊢ 𝐵 = {𝑥 ∣ 𝜑}

Assertion

Ref	Expression
elab2	⊢ (𝐴 ∈ 𝐵 ↔ 𝜓)

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)

Proof of Theorem elab2

Step	Hyp	Ref	Expression
1		elab2.1	. 2 ⊢ 𝐴 ∈ V
2		elab2.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3		elab2.3	. . 3 ⊢ 𝐵 = {𝑥 ∣ 𝜑}
4	2, 3	elab2g 3347	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ 𝜓))
5	1, 4	ax-mp 5	1 ⊢ (𝐴 ∈ 𝐵 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1481   ∈ wcel 1988  {cab 2606  Vcvv 3195

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197

This theorem is referenced by:  elpw  4155  elint  4472  opabid  4972  elrn2  5354  elimasn  5478  oprabid  6662  wfrlem3a  7402  tfrlem3a  7458  cardprclem  8790  iunfictbso  8922  aceq3lem  8928  dfac5lem4  8934  kmlem9  8965  domtriomlem  9249  ltexprlem3  9845  ltexprlem4  9846  reclem2pr  9855  reclem3pr  9856  supsrlem  9917  supaddc  10975  supadd  10976  supmul1  10977  supmullem1  10978  supmullem2  10979  supmul  10980  sqrlem6  13969  infcvgaux2i  14571  mertenslem1  14597  mertenslem2  14598  4sqlem12  15641  conjnmzb  17676  sylow3lem2  18024  mdetunilem9  20407  txuni2  21349  xkoopn  21373  met2ndci  22308  2sqlem8  25132  2sqlem11  25135  eulerpartlemt  30407  eulerpartlemr  30410  eulerpartlemn  30417  subfacp1lem3  31138  subfacp1lem5  31140  soseq  31725  finxpsuclem  33205  heiborlem1  33581  heiborlem6  33586  heiborlem8  33588  cllem0  37690