Theorem elab2g 3633

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  {cab 2738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835

This theorem is used by:  elab2  3635  elab4g  3636  elrab  3644  eldif  4049  elin  4093  elun  4152  elpwg  4559  elsng  4597  elprg  4606  eluni  4869  elintg  4914  eliun  4954  eliin  4955  elopabw  5499  elxpi  5672  elrn2g  5871  eldmg  5879  dmopabelb  5897  elrnmpt  5939  elrnmpt1  5941  elimag  6059  elong  6370  elrnmpog  7555  elrnmpores  7558  eloprabi  8074  orderseqlem  8174  frrlem13  8317  tfrlem12  8398  elqsg  8785  fsetfocdm  8884  elixp2  8930  setrec1lem1  9967  isacn  10124  isfin1a  10371  isfin2  10373  isfin4  10376  isfin7  10380  isfin3ds  10408  elwina  10772  elina  10773  iswun  10790  eltskg  10836  elgrug  10878  elnp  11073  elnpi  11074  iscat  17847  isps  18743  isdir  18773  ismgm  18818  elefmndbas2  19071  elsymgbas2  19588  mdetunilem9  22936  istopg  23214  isbasisg  23266  isptfin  23836  isufl  24233  isusp  24581  2sqlem9  27755  elno  28004  elz12s  28859  isuhgr  29639  isushgr  29640  isupgr  29663  isumgr  29674  isuspgr  29734  isusgr  29735  cplgruvtxb  29995  isacycgr  30752  isacycgr1  30753  isconngr  30791  isconngr1  30792  isplig  31079  isgrpo  31100  elunop  32475  adjeu  32492  isarchi  33786  ispcmp  34532  eulerpartlemelr  35032  eulerpartlemgs2  35055  ballotlemfmpn  35170  elkarden  35872  ismfs  36383  dfon2lem3  36622  elaltxp  36815  elttcirr  37394  bj-ismoore  38101  heiborlem1  38821  heiborlem10  38830  isass  38856  isexid  38857  ismgmOLD  38860  elghomlem2OLD  38896  elcoeleqvrels  39687  eleldisjs  39836  gneispace2  45208  ismnu  45321  nzss  45377  elrnmptf  46272  issal  47400  ismea  47537  isome  47580  ismgmALT  49396  eloprab1st2nd  50054