Theorem elab3 3641

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 3640	. 2 ⊢ ((𝜓 → 𝐴 ∈ 𝑉) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	1, 3	ax-mp 5	1 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)

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

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811

This theorem is referenced by:  fvelrnb  6894  elrnmpo  7494  ovelrn  7534  isfi  8912  isnum2  9857  pm54.43lem  9912  isfin3  10206  isfin5  10209  isfin6  10210  genpelv  10911  iswrd  14438  4sqlem2  16877  vdwapval  16901  isghm  19144  isghmOLD  19145  issrng  20777  ellspsn  20954  lspprel  21046  iscss  21638  ellspd  21757  istps  22878  islp  23084  is2ndc  23390  elpt  23516  itg2l  25686  elply  26156  isismt  28606  bj-ififc  36782  isline  39995  ispointN  39998  ispsubsp  40001  ispsubclN  40193  islaut  40339  ispautN  40355  istendo  41016  sn-isghm  42912  rngunsnply  43407