Theorem elab3 3648

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146  {cab 2744

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841

This theorem is used by:  fvelrnb  6948  elrnmpo  7559  ovelrn  7599  isfi  8981  isnum2  9950  pm54.43lem  10005  isfin3  10298  isfin5  10301  isfin6  10302  genpelv  11003  iswrd  14572  4sqlem2  17034  vdwapval  17058  isghm  19317  issrng  20984  ellspsn  21161  lspprel  21252  iscss  21870  ellspd  21989  istps  23128  islp  23334  is2ndc  23640  elpt  23766  itg2l  25925  elply  26389  isismt  28840  bj-ififc  37216  isline  40554  ispointN  40557  ispsubsp  40560  ispsubclN  40752  islaut  40898  ispautN  40914  istendo  41575  sn-isghm  43446  rngunsnply  43937