Theorem elab2g 2950

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 2296	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
3		elab2g.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	elabg 2949	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
5	2, 4	bitrid 192	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   ∈ wcel 2200  {cab 2215

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801

This theorem is referenced by:  elab2  2951  elab4g  2952  eldif  3206  elun  3345  elin  3387  elif  3614  elsng  3681  elprg  3686  eluni  3891  eliun  3969  eliin  3970  elopab  4347  elong  4465  opeliunxp  4776  elrn2g  4915  eldmg  4921  elrnmpt  4976  elrnmpt1  4978  elimag  5075  elrnmpog  6126  eloprabi  6353  tfrlem3ag  6466  tfr1onlem3ag  6494  tfrcllemsucaccv  6511  elqsg  6745  elixp2  6862  isomni  7319  ismkv  7336  iswomni  7348  isacnm  7401  1idprl  7793  1idpru  7794  recexprlemell  7825  recexprlemelu  7826  mertenslemub  12066  mertenslemi1  12067  mertenslem2  12068  4sqexercise1  12942  4sqexercise2  12943  4sqlemsdc  12944  ismgm  13411  istopg  14694  isbasisg  14739  2sqlem8  15823  2sqlem9  15824  isuhgrm  15892  isushgrm  15893  isupgren  15916  isumgren  15926  isuspgren  15976  isusgren  15977