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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2147  {cab 2741

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839

This theorem is used by:  elab2  3639  elab4g  3640  elrab  3648  eldif  4052  elin  4096  elun  4155  elpwg  4563  elsng  4598  elprg  4607  eluni  4873  elintg  4918  eliun  4958  eliin  4959  elopabw  5504  elxpi  5677  elrn2g  5879  eldmg  5887  dmopabelb  5905  elrnmpt  5947  elrnmpt1  5949  elimag  6072  elong  6388  elrnmpog  7579  elrnmpores  7582  eloprabi  8099  orderseqlem  8201  frrlem13  8344  tfrlem12  8425  elqsg  8812  fsetfocdm  8911  elixp2  8957  setrec1lem1  9993  isacn  10150  isfin1a  10397  isfin2  10399  isfin4  10402  isfin7  10406  isfin3ds  10434  elwina  10798  elina  10799  iswun  10816  eltskg  10862  elgrug  10904  elnp  11099  elnpi  11100  iscat  17875  isps  18771  isdir  18801  ismgm  18846  elefmndbas2  19099  elsymgbas2  19617  mdetunilem9  22965  istopg  23243  isbasisg  23295  isptfin  23865  isufl  24262  isusp  24610  2sqlem9  27784  elno  28033  elz12s  28888  isuhgr  29668  isushgr  29669  isupgr  29692  isumgr  29703  isuspgr  29763  isusgr  29764  cplgruvtxb  30024  isacycgr  30781  isacycgr1  30782  isconngr  30820  isconngr1  30821  isplig  31108  isgrpo  31129  elunop  32504  adjeu  32521  isarchi  33813  ispcmp  34559  eulerpartlemelr  35059  eulerpartlemgs2  35082  ballotlemfmpn  35197  elkarden  35923  ismfs  36481  dfon2lem3  36725  elaltxp  36918  elttcirr  37497  bj-ismoore  38217  heiborlem1  38937  heiborlem10  38946  isass  38972  isexid  38973  ismgmOLD  38976  elghomlem2OLD  39012  elcoeleqvrels  39803  eleldisjs  39952  gneispace2  45324  ismnu  45437  nzss  45493  elrnmptf  46401  issal  47529  ismea  47666  isome  47709  ismgmALT  49525  eloprab1st2nd  50184