Theorem elab3 3629

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811

This theorem is referenced by:  fvelrnb  6900  elrnmpo  7503  ovelrn  7543  isfi  8922  isnum2  9869  pm54.43lem  9924  isfin3  10218  isfin5  10221  isfin6  10222  genpelv  10923  iswrd  14477  4sqlem2  16920  vdwapval  16944  isghm  19190  isghmOLD  19191  issrng  20821  ellspsn  20998  lspprel  21089  iscss  21663  ellspd  21782  istps  22899  islp  23105  is2ndc  23411  elpt  23537  itg2l  25696  elply  26160  isismt  28602  bj-ififc  36847  isline  40185  ispointN  40188  ispsubsp  40191  ispsubclN  40383  islaut  40529  ispautN  40545  istendo  41206  sn-isghm  43106  rngunsnply  43597