Theorem elab3 3665

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  {cab 2713

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809

This theorem is referenced by:  fvelrnb  6938  elrnmpo  7541  ovelrn  7581  isfi  8988  isnum2  9957  pm54.43lem  10012  isfin3  10308  isfin5  10311  isfin6  10312  genpelv  11012  iswrd  14531  4sqlem2  16967  vdwapval  16991  isghm  19196  isghmOLD  19197  issrng  20802  ellspsn  20958  lspprel  21050  iscss  21641  ellspd  21760  istps  22870  islp  23076  is2ndc  23382  elpt  23508  itg2l  25680  elply  26150  isismt  28459  bj-ififc  36546  isline  39704  ispointN  39707  ispsubsp  39710  ispsubclN  39902  islaut  40048  ispautN  40064  istendo  40725  sn-isghm  42643  rngunsnply  43140