Theorem elab2g 3638

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {cab 2707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803

This theorem is referenced by:  elab2  3640  elab4g  3641  elrab  3650  eldif  3915  elin  3921  elun  4106  elpwg  4556  elsng  4593  elprg  4602  eluni  4864  elint  4905  elintg  4907  eliun  4948  eliin  4949  elopabw  5473  elxpi  5645  elrn2g  5837  eldmg  5845  dmopabelb  5863  elrnmpt  5904  elrnmpt1  5906  elimag  6019  elong  6319  elrnmpog  7488  elrnmpores  7491  eloprabi  8005  orderseqlem  8097  frrlem13  8238  tfrlem12  8318  elqsg  8698  fsetfocdm  8795  elixp2  8835  isacn  9957  isfin1a  10205  isfin2  10207  isfin4  10210  isfin7  10214  isfin3ds  10242  elwina  10599  elina  10600  iswun  10617  eltskg  10663  elgrug  10705  elnp  10900  elnpi  10901  iscat  17596  isps  18492  isdir  18522  ismgm  18533  elefmndbas2  18766  elsymgbas2  19270  mdetunilem9  22523  istopg  22798  isbasisg  22850  isptfin  23419  isufl  23816  isusp  24165  2sqlem9  27354  elno  27573  elnoOLD  27574  elzs12  28368  isuhgr  29023  isushgr  29024  isupgr  29047  isumgr  29058  isuspgr  29115  isusgr  29116  cplgruvtxb  29376  isconngr  30151  isconngr1  30152  isplig  30438  isgrpo  30459  elunop  31834  adjeu  31851  isarchi  33134  ispcmp  33823  eulerpartlemelr  34324  eulerpartlemgs2  34347  ballotlemfmpn  34462  isacycgr  35117  isacycgr1  35118  ismfs  35521  dfon2lem3  35758  elaltxp  35948  bj-ismoore  37078  heiborlem1  37790  heiborlem10  37799  isass  37825  isexid  37826  ismgmOLD  37829  elghomlem2OLD  37865  elcoeleqvrels  38571  eleldisjs  38705  gneispace2  44105  ismnu  44234  nzss  44290  elrnmptf  45159  issal  46296  ismea  46433  isome  46476  ismgmALT  48195  eloprab1st2nd  48840  setrec1lem1  49660