Theorem elab2g 3611

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2106  {cab 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816

This theorem is referenced by:  elab2  3613  elab4g  3614  elrab  3624  eldif  3897  elin  3903  elun  4083  elpwg  4536  elsng  4575  elprg  4582  dfopif  4800  eluni  4842  elint  4885  elintg  4887  eliun  4928  eliin  4929  elopabw  5439  elxpi  5611  elrn2g  5799  eldmg  5807  dmopabelb  5825  elrnmpt  5865  elrnmpt1  5867  elimag  5973  elong  6274  elrnmpog  7409  elrnmpores  7411  eloprabi  7903  frrlem13  8114  tfrlem12  8220  elqsg  8557  fsetfocdm  8649  elixp2  8689  isacn  9800  isfin1a  10048  isfin2  10050  isfin4  10053  isfin7  10057  isfin3ds  10085  elwina  10442  elina  10443  iswun  10460  eltskg  10506  elgrug  10548  elnp  10743  elnpi  10744  iscat  17381  isps  18286  isdir  18316  ismgm  18327  elefmndbas2  18513  elsymgbas2  18980  mdetunilem9  21769  istopg  22044  isbasisg  22097  isptfin  22667  isufl  23064  isusp  23413  2sqlem9  26575  isuhgr  27430  isushgr  27431  isupgr  27454  isumgr  27465  isuspgr  27522  isusgr  27523  cplgruvtxb  27780  isconngr  28553  isconngr1  28554  isplig  28838  isgrpo  28859  elunop  30234  adjeu  30251  isarchi  31436  ispcmp  31807  eulerpartlemelr  32324  eulerpartlemgs2  32347  ballotlemfmpn  32461  isacycgr  33107  isacycgr1  33108  ismfs  33511  dfon2lem3  33761  orderseqlem  33801  elno  33849  elaltxp  34277  bj-ismoore  35276  heiborlem1  35969  heiborlem10  35978  isass  36004  isexid  36005  ismgmOLD  36008  elghomlem2OLD  36044  elcoeleqvrels  36708  eleldisjs  36839  gneispace2  41742  ismnu  41879  nzss  41935  elrnmptf  42718  issal  43855  ismea  43989  isome  44032  ismgmALT  45417  setrec1lem1  46393