Theorem elab2g 3680

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  {cab 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816

This theorem is referenced by:  elab2  3682  elab4g  3683  elrab  3692  eldif  3961  elin  3967  elun  4153  elpwg  4603  elsng  4640  elprg  4648  eluni  4910  elint  4952  elintg  4954  eliun  4995  eliin  4996  elopabw  5531  elxpi  5707  elrn2g  5901  eldmg  5909  dmopabelb  5927  elrnmpt  5969  elrnmpt1  5971  elimag  6082  elong  6392  elrnmpog  7568  elrnmpores  7571  eloprabi  8088  orderseqlem  8182  frrlem13  8323  tfrlem12  8429  elqsg  8808  fsetfocdm  8901  elixp2  8941  isacn  10084  isfin1a  10332  isfin2  10334  isfin4  10337  isfin7  10341  isfin3ds  10369  elwina  10726  elina  10727  iswun  10744  eltskg  10790  elgrug  10832  elnp  11027  elnpi  11028  iscat  17715  isps  18613  isdir  18643  ismgm  18654  elefmndbas2  18887  elsymgbas2  19390  mdetunilem9  22626  istopg  22901  isbasisg  22954  isptfin  23524  isufl  23921  isusp  24270  2sqlem9  27471  elno  27690  elnoOLD  27691  elzs12  28421  isuhgr  29077  isushgr  29078  isupgr  29101  isumgr  29112  isuspgr  29169  isusgr  29170  cplgruvtxb  29430  isconngr  30208  isconngr1  30209  isplig  30495  isgrpo  30516  elunop  31891  adjeu  31908  isarchi  33189  ispcmp  33856  eulerpartlemelr  34359  eulerpartlemgs2  34382  ballotlemfmpn  34497  isacycgr  35150  isacycgr1  35151  ismfs  35554  dfon2lem3  35786  elaltxp  35976  bj-ismoore  37106  heiborlem1  37818  heiborlem10  37827  isass  37853  isexid  37854  ismgmOLD  37857  elghomlem2OLD  37893  elcoeleqvrels  38596  eleldisjs  38729  gneispace2  44145  ismnu  44280  nzss  44336  elrnmptf  45186  issal  46329  ismea  46466  isome  46509  ismgmALT  48139  setrec1lem1  49206