Theorem elab2g 3663

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539   ∈ wcel 2107  {cab 2712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808

This theorem is referenced by:  elab2  3665  elab4g  3666  elrab  3675  eldif  3941  elin  3947  elun  4133  elpwg  4583  elsng  4620  elprg  4628  eluni  4890  elint  4932  elintg  4934  eliun  4975  eliin  4976  elopabw  5511  elxpi  5687  elrn2g  5881  eldmg  5889  dmopabelb  5907  elrnmpt  5949  elrnmpt1  5951  elimag  6062  elong  6371  elrnmpog  7550  elrnmpores  7553  eloprabi  8070  orderseqlem  8164  frrlem13  8305  tfrlem12  8411  elqsg  8790  fsetfocdm  8883  elixp2  8923  isacn  10066  isfin1a  10314  isfin2  10316  isfin4  10319  isfin7  10323  isfin3ds  10351  elwina  10708  elina  10709  iswun  10726  eltskg  10772  elgrug  10814  elnp  11009  elnpi  11010  iscat  17686  isps  18582  isdir  18612  ismgm  18623  elefmndbas2  18856  elsymgbas2  19358  mdetunilem9  22574  istopg  22849  isbasisg  22901  isptfin  23470  isufl  23867  isusp  24216  2sqlem9  27407  elno  27626  elnoOLD  27627  elzs12  28357  isuhgr  29005  isushgr  29006  isupgr  29029  isumgr  29040  isuspgr  29097  isusgr  29098  cplgruvtxb  29358  isconngr  30136  isconngr1  30137  isplig  30423  isgrpo  30444  elunop  31819  adjeu  31836  isarchi  33128  ispcmp  33815  eulerpartlemelr  34318  eulerpartlemgs2  34341  ballotlemfmpn  34456  isacycgr  35109  isacycgr1  35110  ismfs  35513  dfon2lem3  35745  elaltxp  35935  bj-ismoore  37065  heiborlem1  37777  heiborlem10  37786  isass  37812  isexid  37813  ismgmOLD  37816  elghomlem2OLD  37852  elcoeleqvrels  38555  eleldisjs  38688  gneispace2  44107  ismnu  44237  nzss  44293  elrnmptf  45143  issal  46286  ismea  46423  isome  46466  ismgmALT  48097  setrec1lem1  49214