Theorem elab3 3579

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1658   ∈ wcel 2166  {cab 2811  Vcvv 3414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416

This theorem is referenced by:  fvelrnb  6490  elrnmpt2  7033  ovelrn  7070  isfi  8246  isnum2  9084  pm54.43lem  9138  isfin3  9433  isfin5  9436  isfin6  9437  genpelv  10137  iswrd  13576  4sqlem2  16024  vdwapval  16048  isghm  18011  issrng  19206  lspsnel  19362  lspprel  19453  iscss  20390  ellspd  20508  istps  21109  islp  21315  is2ndc  21620  elpt  21746  itg2l  23895  elply  24350  isismt  25846  isline  35814  ispointN  35817  ispsubsp  35820  ispsubclN  36012  islaut  36158  ispautN  36174  istendo  36835  rngunsnply  38586