Theorem elab2g 3624

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 3620	. 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  3626  elab4g  3627  elrab  3635  eldif  3900  elin  3906  elun  4094  elpwg  4545  elsng  4582  elprg  4591  eluni  4854  elintg  4898  eliun  4938  eliin  4939  elopabw  5481  elxpi  5653  elrn2g  5846  eldmg  5854  dmopabelb  5872  elrnmpt  5914  elrnmpt1  5916  elimag  6030  elong  6332  elrnmpog  7502  elrnmpores  7505  eloprabi  8016  orderseqlem  8107  frrlem13  8248  tfrlem12  8328  elqsg  8710  fsetfocdm  8808  elixp2  8849  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  17638  isps  18534  isdir  18564  ismgm  18609  elefmndbas2  18842  elsymgbas2  19348  mdetunilem9  22585  istopg  22860  isbasisg  22912  isptfin  23481  isufl  23878  isusp  24226  2sqlem9  27390  elno  27609  elnoOLD  27610  elz12s  28464  isuhgr  29129  isushgr  29130  isupgr  29153  isumgr  29164  isuspgr  29221  isusgr  29222  cplgruvtxb  29482  isconngr  30259  isconngr1  30260  isplig  30547  isgrpo  30568  elunop  31943  adjeu  31960  isarchi  33243  ispcmp  34001  eulerpartlemelr  34501  eulerpartlemgs2  34524  ballotlemfmpn  34639  isacycgr  35327  isacycgr1  35328  ismfs  35731  dfon2lem3  35965  elaltxp  36157  elttcirr  36713  bj-ismoore  37417  heiborlem1  38132  heiborlem10  38141  isass  38167  isexid  38168  ismgmOLD  38171  elghomlem2OLD  38207  elcoeleqvrels  39000  eleldisjs  39149  gneispace2  44559  ismnu  44688  nzss  44744  elrnmptf  45611  issal  46742  ismea  46879  isome  46922  ismgmALT  48693  eloprab1st2nd  49337  setrec1lem1  50156