Theorem elab3 3675

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533   ∈ wcel 2098  {cab 2704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805

This theorem is referenced by:  fvelrnb  6962  elrnmpo  7561  ovelrn  7601  isfi  9001  isnum2  9974  pm54.43lem  10029  isfin3  10325  isfin5  10328  isfin6  10329  genpelv  11029  iswrd  14504  4sqlem2  16923  vdwapval  16947  isghm  19175  issrng  20735  lspsnel  20892  lspprel  20984  iscss  21620  ellspd  21741  istps  22854  islp  23062  is2ndc  23368  elpt  23494  itg2l  25677  elply  26147  isismt  28356  bj-ififc  36063  isline  39216  ispointN  39219  ispsubsp  39222  ispsubclN  39414  islaut  39560  ispautN  39576  istendo  40237  rngunsnply  42600