Theorem elab2g 3624

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812

This theorem is referenced by:  elab2  3626  elab4g  3627  elrab  3635  eldif  3900  elin  3906  elun  4094  elpwg  4545  elsng  4582  elprg  4591  eluni  4854  elint  4896  elintg  4898  eliun  4938  eliin  4939  elopabw  5472  elxpi  5644  elrn2g  5837  eldmg  5845  dmopabelb  5863  elrnmpt  5905  elrnmpt1  5907  elimag  6021  elong  6323  elrnmpog  7493  elrnmpores  7496  eloprabi  8007  orderseqlem  8098  frrlem13  8239  tfrlem12  8319  elqsg  8701  fsetfocdm  8799  elixp2  8840  isacn  9955  isfin1a  10203  isfin2  10205  isfin4  10208  isfin7  10212  isfin3ds  10240  elwina  10598  elina  10599  iswun  10616  eltskg  10662  elgrug  10704  elnp  10899  elnpi  10900  iscat  17596  isps  18492  isdir  18522  ismgm  18567  elefmndbas2  18800  elsymgbas2  19306  mdetunilem9  22563  istopg  22838  isbasisg  22890  isptfin  23459  isufl  23856  isusp  24204  2sqlem9  27378  elno  27597  elnoOLD  27598  elz12s  28452  isuhgr  29117  isushgr  29118  isupgr  29141  isumgr  29152  isuspgr  29209  isusgr  29210  cplgruvtxb  29470  isconngr  30248  isconngr1  30249  isplig  30536  isgrpo  30557  elunop  31932  adjeu  31949  isarchi  33248  ispcmp  34007  eulerpartlemelr  34507  eulerpartlemgs2  34530  ballotlemfmpn  34645  isacycgr  35333  isacycgr1  35334  ismfs  35737  dfon2lem3  35971  elaltxp  36163  elttcirr  36719  bj-ismoore  37415  heiborlem1  38123  heiborlem10  38132  isass  38158  isexid  38159  ismgmOLD  38162  elghomlem2OLD  38198  elcoeleqvrels  38991  eleldisjs  39140  gneispace2  44562  ismnu  44691  nzss  44747  elrnmptf  45614  issal  46746  ismea  46883  isome  46926  ismgmALT  48657  eloprab1st2nd  49301  setrec1lem1  50120