Theorem elab3 3674

Description: Membership in a class abstraction using implicit substitution. (Contributed by NM, 10-Nov-2000.)

Hypotheses

Ref	Expression
elab3.1	⊢ (𝜓 → 𝐴 ∈ V)
elab3.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
elab3	⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elab3

Step	Hyp	Ref	Expression
1		elab3.1	. 2 ⊢ (𝜓 → 𝐴 ∈ V)
2		elab3.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	elab3g 3673	. 2 ⊢ ((𝜓 → 𝐴 ∈ V) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	1, 3	ax-mp 5	1 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533   ∈ wcel 2110  {cab 2799  Vcvv 3495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497

This theorem is referenced by:  fvelrnb  6721  elrnmpo  7281  ovelrn  7318  isfi  8527  isnum2  9368  pm54.43lem  9422  isfin3  9712  isfin5  9715  isfin6  9716  genpelv  10416  iswrd  13857  4sqlem2  16279  vdwapval  16303  isghm  18352  issrng  19615  lspsnel  19769  lspprel  19860  iscss  20821  ellspd  20940  istps  21536  islp  21742  is2ndc  22048  elpt  22174  itg2l  24324  elply  24779  isismt  26314  bj-ififc  33910  isline  36869  ispointN  36872  ispsubsp  36875  ispsubclN  37067  islaut  37213  ispautN  37229  istendo  37890  rngunsnply  39766