Theorem elab2g 2952

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

Hypotheses

Ref	Expression
elab2g.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
elab2g.2	⊢ 𝐵 = {𝑥 ∣ 𝜑}

Assertion

Ref	Expression
elab2g	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓))

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴

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

Proof of Theorem elab2g

Step	Hyp	Ref	Expression
1		elab2g.2	. . 3 ⊢ 𝐵 = {𝑥 ∣ 𝜑}
2	1	eleq2i 2297	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
3		elab2g.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	elabg 2951	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
5	2, 4	bitrid 192	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397   ∈ wcel 2201  {cab 2216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-v 2803

This theorem is referenced by:  elab2  2953  elab4g  2954  eldif  3208  elun  3347  elin  3389  elif  3618  elsng  3685  elprg  3690  eluni  3897  eliun  3975  eliin  3976  elopab  4354  elong  4472  opeliunxp  4783  elrn2g  4922  eldmg  4928  elrnmpt  4983  elrnmpt1  4985  elimag  5082  elrnmpog  6139  eloprabi  6366  tfrlem3ag  6480  tfr1onlem3ag  6508  tfrcllemsucaccv  6525  elqsg  6759  elixp2  6876  isomni  7340  ismkv  7357  iswomni  7369  isacnm  7423  1idprl  7815  1idpru  7816  recexprlemell  7847  recexprlemelu  7848  mertenslemub  12118  mertenslemi1  12119  mertenslem2  12120  4sqexercise1  12994  4sqexercise2  12995  4sqlemsdc  12996  ismgm  13463  istopg  14752  isbasisg  14797  2sqlem8  15881  2sqlem9  15882  isuhgrm  15951  isushgrm  15952  isupgren  15975  isumgren  15985  isuspgren  16037  isusgren  16038