Theorem elab2g 3633

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835

This theorem is used by:  elab2  3635  elab4g  3636  elrab  3644  eldif  3908  elin  3914  elun  4099  elpwg  4559  elsng  4597  elprg  4606  eluni  4869  elintg  4914  eliun  4954  eliin  4955  elopabw  5496  elxpi  5669  elrn2g  5868  eldmg  5876  dmopabelb  5894  elrnmpt  5936  elrnmpt1  5938  elimag  6054  elong  6359  elrnmpog  7543  elrnmpores  7546  eloprabi  8057  orderseqlem  8152  frrlem13  8294  tfrlem12  8375  elqsg  8762  fsetfocdm  8861  elixp2  8907  setrec1lem1  9938  isacn  10095  isfin1a  10342  isfin2  10344  isfin4  10347  isfin7  10351  isfin3ds  10379  elwina  10743  elina  10744  iswun  10761  eltskg  10807  elgrug  10849  elnp  11044  elnpi  11045  iscat  17808  isps  18704  isdir  18734  ismgm  18779  elefmndbas2  19032  elsymgbas2  19549  mdetunilem9  22897  istopg  23175  isbasisg  23227  isptfin  23797  isufl  24194  isusp  24542  2sqlem9  27718  elno  27937  elz12s  28792  isuhgr  29572  isushgr  29573  isupgr  29596  isumgr  29607  isuspgr  29667  isusgr  29668  cplgruvtxb  29928  isacycgr  30685  isacycgr1  30686  isconngr  30724  isconngr1  30725  isplig  31012  isgrpo  31033  elunop  32408  adjeu  32425  isarchi  33677  ispcmp  34423  eulerpartlemelr  34924  eulerpartlemgs2  34947  ballotlemfmpn  35062  elkarden  35748  ismfs  36235  dfon2lem3  36469  elaltxp  36662  elttcirr  37241  bj-ismoore  37946  heiborlem1  38665  heiborlem10  38674  isass  38700  isexid  38701  ismgmOLD  38704  elghomlem2OLD  38740  elcoeleqvrels  39531  eleldisjs  39680  gneispace2  45076  ismnu  45189  nzss  45245  elrnmptf  46117  issal  47246  ismea  47383  isome  47426  ismgmALT  49242  eloprab1st2nd  49900