Theorem elab2 3633

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 3631	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ 𝜓))
5	1, 4	ax-mp 5	1 ⊢ (𝐴 ∈ 𝐵 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111  {cab 2709  Vcvv 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806

This theorem is referenced by:  opabidw  5467  opabid  5468  oprabidw  7383  oprabid  7384  soseq  8095  tfrlem3a  8302  fsetfcdm  8790  cardprclem  9878  iunfictbso  10011  aceq3lem  10017  dfac5lem4  10023  dfac5lem4OLD  10025  kmlem9  10056  domtriomlem  10339  ltexprlem3  10935  ltexprlem4  10936  reclem2pr  10945  reclem3pr  10946  supsrlem  11008  supaddc  12095  supadd  12096  supmul1  12097  supmullem1  12098  supmullem2  12099  supmul  12100  01sqrexlem6  15160  infcvgaux2i  15771  mertenslem1  15797  mertenslem2  15798  4sqlem12  16874  conjnmzb  19171  sylow3lem2  19546  mdetunilem9  22541  txuni2  23486  xkoopn  23510  met2ndci  24443  2sqlem8  27370  2sqlem11  27373  madef  27803  eulerpartlemt  34391  eulerpartlemr  34394  eulerpartlemn  34401  subfacp1lem3  35233  subfacp1lem5  35235  rdgssun  37429  finxpsuclem  37448  heiborlem1  37857  heiborlem6  37862  heiborlem8  37864  cllem0  43664  brpermmodel  45101  fsetsnf  47156  fsetsnfo  47158  cfsetsnfsetf  47163  cfsetsnfsetf1  47164  cfsetsnfsetfo  47165