Theorem dfsbcq 1442

Description: This theorem, which is similar to Theorem 6.7 of [Quine] p. 42, provides us a weak definition of the proper substitution of a class for a set that we will use in place of df-sbc 1441 above. We derive all our results from starting from here instead of df-sbc 1441; in particular, substitution will become undefined when A or B is a proper class. This will leave unspecified the "official" behavior for proper classes, which could be as in the sbc5 1452 assertion (always false) or as in sbc6 1453 (always true) or some more meaningful possibility in the future, that some clever person may discover, that is closer to Quine's definition. (Quine's actual definition cannot be expressed simply in our formal system.)

Assertion

Ref	Expression
dfsbcq	|- (A = B -> ([A / x]ph <-> [B / x]ph))

Proof of Theorem dfsbcq

Step	Hyp	Ref	Expression
1		eleq1 1149	. 2 |- (A = B -> (A e. {x | ph} <-> B e. {x | ph}))
2		df-sbc 1441	. 2 |- ([A / x]ph <-> A e. {x | ph})
3		df-sbc 1441	. 2 |- ([B / x]ph <-> B e. {x | ph})
4	1, 2, 3	3bitr4g 428	1 |- (A = B -> ([A / x]ph <-> [B / x]ph))

Syntax hints:   -> wi 2   <-> wb 127  {cab 1090   = wceq 1091   e. wcel 1092  [wsbc 1440

This theorem is referenced by:  sbceq1 1443  a4sbc 1444  hbsbcg 1445  sbcco 1448  sbcco2 1449  sbcn 1459  sbcim 1460  sbcan 1461  sbcor 1462  sbcbi 1463  sbcal 1464  sbcex 1465  findes 2400  tfindes 2404  nn1suc 4435  uzind 4603  nn0ind 4612  seqlem1 4662

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-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-cleq 1097  df-clel 1099  df-sbc 1441

metamath.org