Theorem elab2g 3669

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ∈ wcel 2099  {cab 2705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806

This theorem is referenced by:  elab2  3671  elab4g  3672  elrab  3682  eldif  3957  elin  3963  elun  4147  elpwg  4606  elsng  4643  elprg  4650  eluni  4911  elint  4955  elintg  4957  eliun  5000  eliin  5001  elopabw  5528  elxpi  5700  elrn2g  5893  eldmg  5901  dmopabelb  5919  elrnmpt  5958  elrnmpt1  5960  elimag  6067  elong  6377  elrnmpog  7556  elrnmpores  7559  eloprabi  8067  orderseqlem  8162  frrlem13  8303  tfrlem12  8409  elqsg  8786  fsetfocdm  8879  elixp2  8919  isacn  10067  isfin1a  10315  isfin2  10317  isfin4  10320  isfin7  10324  isfin3ds  10352  elwina  10709  elina  10710  iswun  10727  eltskg  10773  elgrug  10815  elnp  11010  elnpi  11011  iscat  17651  isps  18559  isdir  18589  ismgm  18600  elefmndbas2  18825  elsymgbas2  19326  mdetunilem9  22521  istopg  22796  isbasisg  22849  isptfin  23419  isufl  23816  isusp  24165  2sqlem9  27359  elno  27578  isuhgr  28872  isushgr  28873  isupgr  28896  isumgr  28907  isuspgr  28964  isusgr  28965  cplgruvtxb  29225  isconngr  29998  isconngr1  29999  isplig  30285  isgrpo  30306  elunop  31681  adjeu  31698  isarchi  32890  ispcmp  33458  eulerpartlemelr  33977  eulerpartlemgs2  34000  ballotlemfmpn  34114  isacycgr  34755  isacycgr1  34756  ismfs  35159  dfon2lem3  35381  elaltxp  35571  bj-ismoore  36584  heiborlem1  37284  heiborlem10  37293  isass  37319  isexid  37320  ismgmOLD  37323  elghomlem2OLD  37359  elcoeleqvrels  38067  eleldisjs  38200  gneispace2  43562  ismnu  43698  nzss  43754  elrnmptf  44554  issal  45702  ismea  45839  isome  45882  ismgmALT  47285  setrec1lem1  48118