Theorem elab3 3645

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ∈ wcel 2141  {cab 2739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836

This theorem is referenced by:  fvelrnb  6923  elrnmpo  7528  ovelrn  7568  isfi  8952  isnum2  9900  pm54.43lem  9955  isfin3  10250  isfin5  10253  isfin6  10254  genpelv  10955  iswrd  14525  4sqlem2  16968  vdwapval  16992  isghm  19239  issrng  20873  ellspsn  21050  lspprel  21141  iscss  21715  ellspd  21834  istps  22974  islp  23180  is2ndc  23486  elpt  23612  itg2l  25771  elply  26235  isismt  28680  bj-ififc  36989  isline  40327  ispointN  40330  ispsubsp  40333  ispsubclN  40525  islaut  40671  ispautN  40687  istendo  41348  sn-isghm  43219  rngunsnply  43710