Theorem elab3 3676

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ∈ wcel 2114  {cab 2801  Vcvv 3496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498

This theorem is referenced by:  fvelrnb  6728  elrnmpo  7289  ovelrn  7326  isfi  8535  isnum2  9376  pm54.43lem  9430  isfin3  9720  isfin5  9723  isfin6  9724  genpelv  10424  iswrd  13866  4sqlem2  16287  vdwapval  16311  isghm  18360  issrng  19623  lspsnel  19777  lspprel  19868  iscss  20829  ellspd  20948  istps  21544  islp  21750  is2ndc  22056  elpt  22182  itg2l  24332  elply  24787  isismt  26322  bj-ififc  33917  isline  36877  ispointN  36880  ispsubsp  36883  ispsubclN  37075  islaut  37221  ispautN  37237  istendo  37898  rngunsnply  39780