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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  {cab 2711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808

This theorem is referenced by:  elab2  3635  elab4g  3636  elrab  3644  eldif  3909  elin  3915  elun  4104  elpwg  4554  elsng  4591  elprg  4600  eluni  4863  elint  4905  elintg  4907  eliun  4947  eliin  4948  elopabw  5471  elxpi  5643  elrn2g  5837  eldmg  5845  dmopabelb  5863  elrnmpt  5905  elrnmpt1  5907  elimag  6020  elong  6322  elrnmpog  7490  elrnmpores  7493  eloprabi  8004  orderseqlem  8096  frrlem13  8237  tfrlem12  8317  elqsg  8697  fsetfocdm  8794  elixp2  8834  isacn  9945  isfin1a  10193  isfin2  10195  isfin4  10198  isfin7  10202  isfin3ds  10230  elwina  10587  elina  10588  iswun  10605  eltskg  10651  elgrug  10693  elnp  10888  elnpi  10889  iscat  17588  isps  18484  isdir  18514  ismgm  18559  elefmndbas2  18792  elsymgbas2  19295  mdetunilem9  22545  istopg  22820  isbasisg  22872  isptfin  23441  isufl  23838  isusp  24186  2sqlem9  27375  elno  27594  elnoOLD  27595  elzs12  28393  isuhgr  29049  isushgr  29050  isupgr  29073  isumgr  29084  isuspgr  29141  isusgr  29142  cplgruvtxb  29402  isconngr  30180  isconngr1  30181  isplig  30467  isgrpo  30488  elunop  31863  adjeu  31880  isarchi  33162  ispcmp  33881  eulerpartlemelr  34381  eulerpartlemgs2  34404  ballotlemfmpn  34519  isacycgr  35200  isacycgr1  35201  ismfs  35604  dfon2lem3  35838  elaltxp  36030  bj-ismoore  37160  heiborlem1  37861  heiborlem10  37870  isass  37896  isexid  37897  ismgmOLD  37900  elghomlem2OLD  37936  elcoeleqvrels  38701  eleldisjs  38836  gneispace2  44239  ismnu  44368  nzss  44424  elrnmptf  45292  issal  46426  ismea  46563  isome  46606  ismgmALT  48337  eloprab1st2nd  48982  setrec1lem1  49802