Theorem elab2g 3634

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804

This theorem is referenced by:  elab2  3636  elab4g  3637  elrab  3645  eldif  3910  elin  3916  elun  4101  elpwg  4551  elsng  4588  elprg  4597  eluni  4860  elint  4901  elintg  4903  eliun  4943  eliin  4944  elopabw  5464  elxpi  5636  elrn2g  5828  eldmg  5836  dmopabelb  5854  elrnmpt  5895  elrnmpt1  5897  elimag  6010  elong  6310  elrnmpog  7476  elrnmpores  7479  eloprabi  7990  orderseqlem  8082  frrlem13  8223  tfrlem12  8303  elqsg  8683  fsetfocdm  8780  elixp2  8820  isacn  9927  isfin1a  10175  isfin2  10177  isfin4  10180  isfin7  10184  isfin3ds  10212  elwina  10569  elina  10570  iswun  10587  eltskg  10633  elgrug  10675  elnp  10870  elnpi  10871  iscat  17570  isps  18466  isdir  18496  ismgm  18541  elefmndbas2  18774  elsymgbas2  19278  mdetunilem9  22528  istopg  22803  isbasisg  22855  isptfin  23424  isufl  23821  isusp  24169  2sqlem9  27358  elno  27577  elnoOLD  27578  elzs12  28376  isuhgr  29031  isushgr  29032  isupgr  29055  isumgr  29066  isuspgr  29123  isusgr  29124  cplgruvtxb  29384  isconngr  30159  isconngr1  30160  isplig  30446  isgrpo  30467  elunop  31842  adjeu  31859  isarchi  33141  ispcmp  33860  eulerpartlemelr  34360  eulerpartlemgs2  34383  ballotlemfmpn  34498  isacycgr  35157  isacycgr1  35158  ismfs  35561  dfon2lem3  35798  elaltxp  35988  bj-ismoore  37118  heiborlem1  37830  heiborlem10  37839  isass  37865  isexid  37866  ismgmOLD  37869  elghomlem2OLD  37905  elcoeleqvrels  38611  eleldisjs  38745  gneispace2  44144  ismnu  44273  nzss  44329  elrnmptf  45197  issal  46331  ismea  46468  isome  46511  ismgmALT  48233  eloprab1st2nd  48878  setrec1lem1  49698