Theorem elab2g 3322

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977  {cab 2596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175

This theorem is referenced by:  elab2  3323  elab4g  3324  eldif  3550  elun  3715  elin  3758  elsng  4139  elprg  4144  eluni  4375  elintg  4418  eliun  4460  eliin  4461  elopab  4908  elrn2g  5235  eldmg  5241  elrnmpt  5293  elrnmpt1  5295  elimag  5389  elong  5648  elrnmpt2g  6670  elrnmpt2res  6672  eloprabi  7121  tfrlem12  7372  elqsg  7685  elixp2  7798  isacn  8750  isfin1a  8997  isfin2  8999  isfin4  9002  isfin7  9006  isfin3ds  9034  elwina  9387  elina  9388  iswun  9405  eltskg  9451  elgrug  9493  elnp  9688  elnpi  9689  iscat  16156  isps  17025  isdir  17055  ismgm  17066  elsymgbas2  17624  mdetunilem9  20245  istopg  20525  isbasisg  20562  isptfin  21129  isufl  21527  isusp  21875  2sqlem9  24952  isuhgr  25726  isushgr  25727  isupgr  25751  isumgr  25761  isplig  26720  isgrpo  26735  elunop  28115  adjeu  28132  isarchi  29067  ispcmp  29252  eulerpartlemelr  29746  eulerpartlemgs2  29769  ballotlemfmpn  29883  ismfs  30700  dfon2lem3  30934  orderseqlem  30993  elno  31043  elaltxp  31252  heiborlem1  32780  heiborlem10  32789  isass  32815  isexid  32816  ismgmOLD  32819  elghomlem2OLD  32855  gneispace2  37450  nzss  37538  elrnmptf  38362  issal  39210  isuspgr  40382  isusgr  40383  iscplgr  40636  isconngr  41356  isconngr1  41357  isfrgr  41430  ismgmALT  41649