Theorem dfsbcq 1946

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 1945 above. We derive all our results from starting from here instead of df-sbc 1945. As a consequence we can derive elabs 1969, which is a weaker version of df-sbc 1945 that leaves substitution undefined when A is a proper class. We thus leave unspecified the "official" behavior for proper classes, which could be as in the sbc5 1959 assertion (always false) or as in sbc6 1960 (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 directly 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 1537	. 2 |- (A = B -> (A e. {x | ph} <-> B e. {x | ph}))
2		df-sbc 1945	. 2 |- ([A / x]ph <-> A e. {x | ph})
3		df-sbc 1945	. 2 |- ([B / x]ph <-> B e. {x | ph})
4	1, 2, 3	3bitr4g 557	1 |- (A = B -> ([A / x]ph <-> [B / x]ph))

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

This theorem is referenced by:  sbceq1a 1947  a4sbc 1948  hbsbc1g 1951  hbsbcg 1954  sbccog 1955  sbcco2 1956  sbcng 1972  sbcimg 1973  sbcang 1974  sbcorg 1975  sbcbidig 1976  sbcalg 1977  sbcexg 1978  hbsbc1gd 1986  hbsbcgd 1987  ra4sbc 2000  csbeq1 2006  sbcco3g 2044  findes 3166  tfindes 3170  nn1suc 5941  uzindOLD 6210  nn0ind-raph 6216  seq1lem1 6310  uzind4s 6453  uzind4s2 6454  fzrevralt 6520  fzshftralt 6523

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-cleq 1472  df-clel 1475  df-sbc 1945

Copyright terms: Public domain