Theorem elab2g 2963

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   ∈ wcel 2203  {cab 2218

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814

This theorem is referenced by:  elab2  2964  elab4g  2965  eldif  3219  elun  3359  elin  3401  elif  3633  elsng  3703  elprg  3708  eluni  3916  eliun  3994  eliin  3995  elopab  4375  elong  4493  opeliunxp  4804  elrn2g  4944  eldmg  4950  elrnmpt  5005  elrnmpt1  5007  elimag  5104  elrnmpog  6165  eloprabi  6391  tfrlem3ag  6539  tfr1onlem3ag  6567  tfrcllemsucaccv  6584  elqsg  6818  elixp2  6936  isomni  7426  ismkv  7443  iswomni  7455  isacnm  7509  1idprl  7901  1idpru  7902  recexprlemell  7933  recexprlemelu  7934  mertenslemub  12213  mertenslemi1  12214  mertenslem2  12215  4sqexercise1  13089  4sqexercise2  13090  4sqlemsdc  13091  ismgm  13559  istopg  14851  isbasisg  14896  2sqlem8  15983  2sqlem9  15984  isuhgrm  16053  isushgrm  16054  isupgren  16077  isumgren  16087  isuspgren  16139  isusgren  16140