Theorem elab2g 3625

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119  {cab 2718

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815

This theorem is referenced by:  elab2  3627  elab4g  3628  elrab  3636  eldif  3900  elin  3906  elun  4090  elpwg  4539  elsng  4576  elprg  4585  eluni  4848  elintg  4892  eliun  4932  eliin  4933  elopabw  5475  elxpi  5647  elrn2g  5839  eldmg  5847  dmopabelb  5865  elrnmpt  5907  elrnmpt1  5909  elimag  6023  elong  6325  elrnmpog  7498  elrnmpores  7501  eloprabi  8012  orderseqlem  8104  frrlem13  8245  tfrlem12  8325  elqsg  8707  fsetfocdm  8805  elixp2  8846  isacn  9964  isfin1a  10212  isfin2  10214  isfin4  10217  isfin7  10221  isfin3ds  10249  elwina  10607  elina  10608  iswun  10625  eltskg  10671  elgrug  10713  elnp  10908  elnpi  10909  iscat  17636  isps  18532  isdir  18562  ismgm  18607  elefmndbas2  18840  elsymgbas2  19346  mdetunilem9  22610  istopg  22885  isbasisg  22937  isptfin  23506  isufl  23903  isusp  24251  2sqlem9  27415  elno  27634  elnoOLD  27635  elz12s  28489  isuhgr  29154  isushgr  29155  isupgr  29178  isumgr  29189  isuspgr  29246  isusgr  29247  cplgruvtxb  29507  isconngr  30284  isconngr1  30285  isplig  30572  isgrpo  30593  elunop  31968  adjeu  31985  isarchi  33270  ispcmp  34048  eulerpartlemelr  34548  eulerpartlemgs2  34571  ballotlemfmpn  34686  isacycgr  35374  isacycgr1  35375  ismfs  35778  dfon2lem3  36012  elaltxp  36204  elttcirr  36760  bj-ismoore  37464  heiborlem1  38179  heiborlem10  38188  isass  38214  isexid  38215  ismgmOLD  38218  elghomlem2OLD  38254  elcoeleqvrels  39047  eleldisjs  39196  gneispace2  44577  ismnu  44706  nzss  44762  elrnmptf  45629  issal  46758  ismea  46895  isome  46938  ismgmALT  48715  eloprab1st2nd  49359  setrec1lem1  50178