Theorem elab2g 3650

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804

This theorem is referenced by:  elab2  3652  elab4g  3653  elrab  3662  eldif  3927  elin  3933  elun  4119  elpwg  4569  elsng  4606  elprg  4615  eluni  4877  elint  4919  elintg  4921  eliun  4962  eliin  4963  elopabw  5489  elxpi  5663  elrn2g  5857  eldmg  5865  dmopabelb  5883  elrnmpt  5925  elrnmpt1  5927  elimag  6038  elong  6343  elrnmpog  7527  elrnmpores  7530  eloprabi  8045  orderseqlem  8139  frrlem13  8280  tfrlem12  8360  elqsg  8740  fsetfocdm  8837  elixp2  8877  isacn  10004  isfin1a  10252  isfin2  10254  isfin4  10257  isfin7  10261  isfin3ds  10289  elwina  10646  elina  10647  iswun  10664  eltskg  10710  elgrug  10752  elnp  10947  elnpi  10948  iscat  17640  isps  18534  isdir  18564  ismgm  18575  elefmndbas2  18808  elsymgbas2  19310  mdetunilem9  22514  istopg  22789  isbasisg  22841  isptfin  23410  isufl  23807  isusp  24156  2sqlem9  27345  elno  27564  elnoOLD  27565  elzs12  28344  isuhgr  28994  isushgr  28995  isupgr  29018  isumgr  29029  isuspgr  29086  isusgr  29087  cplgruvtxb  29347  isconngr  30125  isconngr1  30126  isplig  30412  isgrpo  30433  elunop  31808  adjeu  31825  isarchi  33143  ispcmp  33854  eulerpartlemelr  34355  eulerpartlemgs2  34378  ballotlemfmpn  34493  isacycgr  35139  isacycgr1  35140  ismfs  35543  dfon2lem3  35780  elaltxp  35970  bj-ismoore  37100  heiborlem1  37812  heiborlem10  37821  isass  37847  isexid  37848  ismgmOLD  37851  elghomlem2OLD  37887  elcoeleqvrels  38593  eleldisjs  38727  gneispace2  44128  ismnu  44257  nzss  44313  elrnmptf  45182  issal  46319  ismea  46456  isome  46499  ismgmALT  48215  eloprab1st2nd  48860  setrec1lem1  49680