Theorem elab3 3688

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813

This theorem is referenced by:  fvelrnb  6968  elrnmpo  7568  ovelrn  7608  isfi  9014  isnum2  9982  pm54.43lem  10037  isfin3  10333  isfin5  10336  isfin6  10337  genpelv  11037  iswrd  14550  4sqlem2  16982  vdwapval  17006  isghm  19245  isghmOLD  19246  issrng  20861  ellspsn  21018  lspprel  21110  iscss  21718  ellspd  21839  istps  22955  islp  23163  is2ndc  23469  elpt  23595  itg2l  25778  elply  26248  isismt  28556  bj-ififc  36564  isline  39721  ispointN  39724  ispsubsp  39727  ispsubclN  39919  islaut  40065  ispautN  40081  istendo  40742  sn-isghm  42659  rngunsnply  43157