Theorem elab2g 2882

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   ∈ wcel 2146  {cab 2161

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737

This theorem is referenced by:  elab2  2883  elab4g  2884  eldif  3136  elun  3274  elin  3316  elsng  3604  elprg  3609  eluni  3808  eliun  3886  eliin  3887  elopab  4252  elong  4367  opeliunxp  4675  elrn2g  4810  eldmg  4815  elrnmpt  4869  elrnmpt1  4871  elimag  4967  elrnmpog  5977  eloprabi  6187  tfrlem3ag  6300  tfr1onlem3ag  6328  tfrcllemsucaccv  6345  elqsg  6575  elixp2  6692  isomni  7124  ismkv  7141  iswomni  7153  1idprl  7564  1idpru  7565  recexprlemell  7596  recexprlemelu  7597  mertenslemub  11510  mertenslemi1  11511  mertenslem2  11512  ismgm  12642  istopg  13068  isbasisg  13113  2sqlem8  14030  2sqlem9  14031