Theorem elabsg 2488

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 2454 but was proved using only dfsbcq 2455 as its starting point (making no other reference to df-sbc 2454). We prefer not to make direct reference to df-sbc 2454 (i.e. commit to it) since its behavior at proper classes is at odds with Quine, whereas dfsbcq 2455 is not. (Quine's class substitution cannot be expressed in closed form.) This theorem serves as a weaker Quine-compatible substitute for df-sbc 2454.

Assertion

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

Proof of Theorem elabsg

Step	Hyp	Ref	Expression
1		elisset 2299	. 2 |- (A e. B -> A e. _V)
2		elabs2 2487	. . 3 |- (A e. {x | ph} <-> (A e. _V /\ [A / x]ph))
3	2	baib 749	. 2 |- (A e. _V -> (A e. {x | ph} <-> [A / x]ph))
4	1, 3	syl 12	1 |- (A e. B -> (A e. {x | ph} <-> [A / x]ph))

Syntax hints:   -> wi 3   <-> wb 163   e. wcel 1300  [wsbc 1534  {cab 1871  _Vcvv 2292

This theorem is referenced by:  bnj1454 13135  bnj984 13358  rusbcALT 16410

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-rab 2112  df-v 2294  df-sbc 2454

Copyright terms: Public domain