Theorem elab3 3638

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

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

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808

This theorem is referenced by:  fvelrnb  6888  elrnmpo  7488  ovelrn  7528  isfi  8904  isnum2  9845  pm54.43lem  9900  isfin3  10194  isfin5  10197  isfin6  10198  genpelv  10898  iswrd  14424  4sqlem2  16863  vdwapval  16887  isghm  19129  isghmOLD  19130  issrng  20761  ellspsn  20938  lspprel  21030  iscss  21622  ellspd  21741  istps  22850  islp  23056  is2ndc  23362  elpt  23488  itg2l  25658  elply  26128  isismt  28513  bj-ififc  36647  isline  39858  ispointN  39861  ispsubsp  39864  ispsubclN  40056  islaut  40202  ispautN  40218  istendo  40879  sn-isghm  42791  rngunsnply  43286