Theorem elabs 1458

Description: Membership in a class abstraction, expressed in terms of class substitution. Conveniently, this theorem has no distinct variable restrictions. Except for the existence hypothesis, this theorem is "almost" like df-sbc 1441 but was proved using only dfsbcq 1442 as its starting point (making no other reference to df-sbc 1441). We prefer not to make direct reference to df-sbc 1441 since its behavior at proper classes is at odds with Quine, whereas dfsbcq 1442 is not. (Quine's class substitution cannot be expressed in closed form.) This theorem serves as a Quine-compatible substitute for df-sbc 1441.

Hypothesis

Ref	Expression
elabs.1	⊢ A ∈ V

Assertion

Ref	Expression
elabs	⊢ (A ∈ {x∣φ} ↔ [A / x]φ)

Proof of Theorem elabs

Step	Hyp	Ref	Expression
1		elabs2 1457	. 2 ⊢ (A ∈ {x∣φ} ↔ (A ∈ V ∧ [A / x]φ))
2		elabs.1	. 2 ⊢ A ∈ V
3	1, 2	mpbiran 547	1 ⊢ (A ∈ {x∣φ} ↔ [A / x]φ)

Syntax hints:   ↔ wb 127  {cab 1090   ∈ wcel 1092  Vcvv 1348  [wsbc 1440

This theorem is referenced by:  hta 3619

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-rab 1208  df-v 1349  df-sbc 1441

metamath.org