Theorem elabsg 1968

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

Assertion

Ref	Expression
elabsg	|- (A e. B -> (A e. {x | ph} <-> [A / x]ph))

Proof of Theorem elabsg

Step	Hyp	Ref	Expression
1		elisset 1820	. 2 |- (A e. B -> A e. V)
2		elabs2 1967	. . 3 |- (A e. {x | ph} <-> (A e. V /\ [A / x]ph))
3	2	baib 687	. 2 |- (A e. V -> (A e. {x | ph} <-> [A / x]ph))
4	1, 3	syl 10	1 |- (A e. B -> (A e. {x | ph} <-> [A / x]ph))

Syntax hints:   -> wi 3   <-> wb 146   e. wcel 960  [wsbc 1172  {cab 1466  Vcvv 1814

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-rab 1655  df-v 1815  df-sbc 1945

Copyright terms: Public domain