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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1554   ∈ wcel 2136  {cab 2734

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1557  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831

This theorem is referenced by:  elab2  3636  elab4g  3637  elrab  3645  eldif  3909  elin  3915  elun  4101  elpwg  4552  elsng  4590  elprg  4599  eluni  4862  elintg  4907  eliun  4947  eliin  4948  elopabw  5490  elxpi  5662  elrn2g  5859  eldmg  5867  dmopabelb  5885  elrnmpt  5927  elrnmpt1  5929  elimag  6043  elong  6343  elrnmpog  7520  elrnmpores  7523  eloprabi  8033  orderseqlem  8125  frrlem13  8267  tfrlem12  8348  elqsg  8733  fsetfocdm  8831  elixp2  8872  isacn  9990  isfin1a  10239  isfin2  10241  isfin4  10244  isfin7  10248  isfin3ds  10276  elwina  10634  elina  10635  iswun  10652  eltskg  10698  elgrug  10740  elnp  10935  elnpi  10936  iscat  17680  isps  18576  isdir  18606  ismgm  18651  elefmndbas2  18884  elsymgbas2  19389  mdetunilem9  22653  istopg  22928  isbasisg  22980  isptfin  23549  isufl  23946  isusp  24294  2sqlem9  27461  elno  27680  elz12s  28535  isuhgr  29200  isushgr  29201  isupgr  29224  isumgr  29235  isuspgr  29292  isusgr  29293  cplgruvtxb  29553  isconngr  30330  isconngr1  30331  isplig  30618  isgrpo  30639  elunop  32014  adjeu  32031  isarchi  33316  ispcmp  34108  eulerpartlemelr  34608  eulerpartlemgs2  34631  ballotlemfmpn  34746  isacycgr  35443  isacycgr1  35444  ismfs  35847  dfon2lem3  36081  elaltxp  36273  elttcirr  36839  bj-ismoore  37543  heiborlem1  38258  heiborlem10  38267  isass  38293  isexid  38294  ismgmOLD  38297  elghomlem2OLD  38333  elcoeleqvrels  39126  eleldisjs  39275  gneispace2  44656  ismnu  44785  nzss  44841  elrnmptf  45707  issal  46836  ismea  46973  isome  47016  ismgmALT  48793  eloprab1st2nd  49437  setrec1lem1  50256