Theorem elab2g 3637

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 3633	. 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  3639  elab4g  3640  elrab  3648  eldif  3913  elin  3919  elun  4107  elpwg  4559  elsng  4596  elprg  4605  eluni  4868  elint  4910  elintg  4912  eliun  4952  eliin  4953  elopabw  5482  elxpi  5654  elrn2g  5847  eldmg  5855  dmopabelb  5873  elrnmpt  5915  elrnmpt1  5917  elimag  6031  elong  6333  elrnmpog  7503  elrnmpores  7506  eloprabi  8017  orderseqlem  8109  frrlem13  8250  tfrlem12  8330  elqsg  8712  fsetfocdm  8810  elixp2  8851  isacn  9966  isfin1a  10214  isfin2  10216  isfin4  10219  isfin7  10223  isfin3ds  10251  elwina  10609  elina  10610  iswun  10627  eltskg  10673  elgrug  10715  elnp  10910  elnpi  10911  iscat  17607  isps  18503  isdir  18533  ismgm  18578  elefmndbas2  18811  elsymgbas2  19314  mdetunilem9  22576  istopg  22851  isbasisg  22903  isptfin  23472  isufl  23869  isusp  24217  2sqlem9  27406  elno  27625  elnoOLD  27626  elz12s  28480  isuhgr  29145  isushgr  29146  isupgr  29169  isumgr  29180  isuspgr  29237  isusgr  29238  cplgruvtxb  29498  isconngr  30276  isconngr1  30277  isplig  30563  isgrpo  30584  elunop  31959  adjeu  31976  isarchi  33275  ispcmp  34034  eulerpartlemelr  34534  eulerpartlemgs2  34557  ballotlemfmpn  34672  isacycgr  35358  isacycgr1  35359  ismfs  35762  dfon2lem3  35996  elaltxp  36188  bj-ismoore  37349  heiborlem1  38051  heiborlem10  38060  isass  38086  isexid  38087  ismgmOLD  38090  elghomlem2OLD  38126  elcoeleqvrels  38919  eleldisjs  39068  gneispace2  44477  ismnu  44606  nzss  44662  elrnmptf  45529  issal  46661  ismea  46798  isome  46841  ismgmALT  48572  eloprab1st2nd  49216  setrec1lem1  50035