Theorem elab2g 3636

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812

This theorem is referenced by:  elab2  3638  elab4g  3639  elrab  3647  eldif  3912  elin  3918  elun  4106  elpwg  4558  elsng  4595  elprg  4604  eluni  4867  elint  4909  elintg  4911  eliun  4951  eliin  4952  elopabw  5475  elxpi  5647  elrn2g  5840  eldmg  5848  dmopabelb  5866  elrnmpt  5908  elrnmpt1  5910  elimag  6024  elong  6326  elrnmpog  7495  elrnmpores  7498  eloprabi  8009  orderseqlem  8101  frrlem13  8242  tfrlem12  8322  elqsg  8704  fsetfocdm  8802  elixp2  8843  isacn  9958  isfin1a  10206  isfin2  10208  isfin4  10211  isfin7  10215  isfin3ds  10243  elwina  10601  elina  10602  iswun  10619  eltskg  10665  elgrug  10707  elnp  10902  elnpi  10903  iscat  17599  isps  18495  isdir  18525  ismgm  18570  elefmndbas2  18803  elsymgbas2  19306  mdetunilem9  22568  istopg  22843  isbasisg  22895  isptfin  23464  isufl  23861  isusp  24209  2sqlem9  27398  elno  27617  elnoOLD  27618  elzs12  28451  isuhgr  29116  isushgr  29117  isupgr  29140  isumgr  29151  isuspgr  29208  isusgr  29209  cplgruvtxb  29469  isconngr  30247  isconngr1  30248  isplig  30534  isgrpo  30555  elunop  31930  adjeu  31947  isarchi  33245  ispcmp  33995  eulerpartlemelr  34495  eulerpartlemgs2  34518  ballotlemfmpn  34633  isacycgr  35320  isacycgr1  35321  ismfs  35724  dfon2lem3  35958  elaltxp  36150  bj-ismoore  37281  heiborlem1  37983  heiborlem10  37992  isass  38018  isexid  38019  ismgmOLD  38022  elghomlem2OLD  38058  elcoeleqvrels  38851  eleldisjs  39000  gneispace2  44409  ismnu  44538  nzss  44594  elrnmptf  45461  issal  46594  ismea  46731  isome  46774  ismgmALT  48505  eloprab1st2nd  49149  setrec1lem1  49968