Theorem elab3 3642

Description: Membership in a class abstraction using implicit substitution. (Contributed by NM, 10-Nov-2000.) (Revised by AV, 16-Aug-2024.)

Hypotheses

Ref	Expression
elab3.1	⊢ (𝜓 → 𝐴 ∈ 𝑉)
elab3.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
elab3	⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem elab3

Step	Hyp	Ref	Expression
1		elab3.1	. 2 ⊢ (𝜓 → 𝐴 ∈ 𝑉)
2		elab3.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	elab3g 3641	. 2 ⊢ ((𝜓 → 𝐴 ∈ 𝑉) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	1, 3	ax-mp 5	1 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)

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

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806

This theorem is referenced by:  fvelrnb  6882  elrnmpo  7482  ovelrn  7522  isfi  8898  isnum2  9835  pm54.43lem  9890  isfin3  10184  isfin5  10187  isfin6  10188  genpelv  10888  iswrd  14419  4sqlem2  16858  vdwapval  16882  isghm  19125  isghmOLD  19126  issrng  20757  ellspsn  20934  lspprel  21026  iscss  21618  ellspd  21737  istps  22847  islp  23053  is2ndc  23359  elpt  23485  itg2l  25655  elply  26125  isismt  28510  bj-ififc  36615  isline  39777  ispointN  39780  ispsubsp  39783  ispsubclN  39975  islaut  40121  ispautN  40137  istendo  40798  sn-isghm  42705  rngunsnply  43201