Theorem elab2g 3634

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 3630	. 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  3636  elab4g  3637  elrab  3645  eldif  3909  elin  3915  elun  4100  elpwg  4560  elsng  4598  elprg  4607  eluni  4870  elintg  4915  eliun  4955  eliin  4956  elopabw  5504  elxpi  5677  elrn2g  5874  eldmg  5882  dmopabelb  5900  elrnmpt  5942  elrnmpt1  5944  elimag  6060  elong  6365  elrnmpog  7549  elrnmpores  7552  eloprabi  8061  orderseqlem  8156  frrlem13  8298  tfrlem12  8379  elqsg  8766  fsetfocdm  8865  elixp2  8911  isacn  10050  isfin1a  10297  isfin2  10299  isfin4  10302  isfin7  10306  isfin3ds  10334  elwina  10698  elina  10699  iswun  10716  eltskg  10762  elgrug  10804  elnp  10999  elnpi  11000  iscat  17763  isps  18659  isdir  18689  ismgm  18734  elefmndbas2  18986  elsymgbas2  19503  mdetunilem9  22845  istopg  23123  isbasisg  23175  isptfin  23745  isufl  24142  isusp  24490  2sqlem9  27666  elno  27885  elz12s  28740  isuhgr  29520  isushgr  29521  isupgr  29544  isumgr  29555  isuspgr  29615  isusgr  29616  cplgruvtxb  29876  isacycgr  30633  isacycgr1  30634  isconngr  30672  isconngr1  30673  isplig  30960  isgrpo  30981  elunop  32356  adjeu  32373  isarchi  33625  ispcmp  34370  eulerpartlemelr  34871  eulerpartlemgs2  34894  ballotlemfmpn  35009  elkarden  35684  ismfs  36131  dfon2lem3  36365  elaltxp  36558  elttcirr  37153  bj-ismoore  37858  heiborlem1  38564  heiborlem10  38573  isass  38599  isexid  38600  ismgmOLD  38603  elghomlem2OLD  38639  elcoeleqvrels  39430  eleldisjs  39579  gneispace2  44975  ismnu  45088  nzss  45144  elrnmptf  46016  issal  47145  ismea  47282  isome  47325  ismgmALT  49141  eloprab1st2nd  49799  setrec1lem1  50616