Theorem elab2 3636

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2110  {cab 2708  Vcvv 3434

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 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804

This theorem is referenced by:  opabidw  5462  opabid  5463  oprabidw  7372  oprabid  7373  soseq  8084  tfrlem3a  8291  fsetfcdm  8779  cardprclem  9864  iunfictbso  9997  aceq3lem  10003  dfac5lem4  10009  dfac5lem4OLD  10011  kmlem9  10042  domtriomlem  10325  ltexprlem3  10921  ltexprlem4  10922  reclem2pr  10931  reclem3pr  10932  supsrlem  10994  supaddc  12081  supadd  12082  supmul1  12083  supmullem1  12084  supmullem2  12085  supmul  12086  01sqrexlem6  15146  infcvgaux2i  15757  mertenslem1  15783  mertenslem2  15784  4sqlem12  16860  conjnmzb  19158  sylow3lem2  19533  mdetunilem9  22528  txuni2  23473  xkoopn  23497  met2ndci  24430  2sqlem8  27357  2sqlem11  27360  madef  27790  eulerpartlemt  34374  eulerpartlemr  34377  eulerpartlemn  34384  subfacp1lem3  35194  subfacp1lem5  35196  rdgssun  37391  finxpsuclem  37410  heiborlem1  37830  heiborlem6  37835  heiborlem8  37837  cllem0  43578  brpermmodel  45015  fsetsnf  47061  fsetsnfo  47063  cfsetsnfsetf  47068  cfsetsnfsetf1  47069  cfsetsnfsetfo  47070