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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2104  {cab 2707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808

This theorem is referenced by:  elab2  3671  elab4g  3672  elrab  3682  eldif  3957  elin  3963  elun  4147  elpwg  4604  elsng  4641  elprg  4648  eluni  4910  elint  4955  elintg  4957  eliun  5000  eliin  5001  elopabw  5525  elxpi  5697  elrn2g  5889  eldmg  5897  dmopabelb  5915  elrnmpt  5954  elrnmpt1  5956  elimag  6062  elong  6371  elrnmpog  7546  elrnmpores  7548  eloprabi  8051  orderseqlem  8145  frrlem13  8285  tfrlem12  8391  elqsg  8764  fsetfocdm  8857  elixp2  8897  isacn  10041  isfin1a  10289  isfin2  10291  isfin4  10294  isfin7  10298  isfin3ds  10326  elwina  10683  elina  10684  iswun  10701  eltskg  10747  elgrug  10789  elnp  10984  elnpi  10985  iscat  17620  isps  18525  isdir  18555  ismgm  18566  elefmndbas2  18791  elsymgbas2  19281  mdetunilem9  22342  istopg  22617  isbasisg  22670  isptfin  23240  isufl  23637  isusp  23986  2sqlem9  27166  elno  27385  isuhgr  28587  isushgr  28588  isupgr  28611  isumgr  28622  isuspgr  28679  isusgr  28680  cplgruvtxb  28937  isconngr  29709  isconngr1  29710  isplig  29996  isgrpo  30017  elunop  31392  adjeu  31409  isarchi  32598  ispcmp  33135  eulerpartlemelr  33654  eulerpartlemgs2  33677  ballotlemfmpn  33791  isacycgr  34434  isacycgr1  34435  ismfs  34838  dfon2lem3  35061  elaltxp  35251  bj-ismoore  36289  heiborlem1  36982  heiborlem10  36991  isass  37017  isexid  37018  ismgmOLD  37021  elghomlem2OLD  37057  elcoeleqvrels  37768  eleldisjs  37901  gneispace2  43185  ismnu  43322  nzss  43378  elrnmptf  44178  issal  45328  ismea  45465  isome  45508  ismgmALT  46899  setrec1lem1  47819