Theorem dfsbcq 1933

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 1932 above. We derive all our results from starting from here instead of df-sbc 1932. As a consequence we can derive elabs 1956, which is a weaker version of df-sbc 1932 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 1946 assertion (always false) or as in sbc6 1947 (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 1526	. 2 |- (A = B -> (A e. {x | ph} <-> B e. {x | ph}))
2		df-sbc 1932	. 2 |- ([A / x]ph <-> A e. {x | ph})
3		df-sbc 1932	. 2 |- ([B / x]ph <-> B e. {x | ph})
4	1, 2, 3	3bitr4g 553	1 |- (A = B -> ([A / x]ph <-> [B / x]ph))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 953   e. wcel 955  [wsbc 1166  {cab 1456

This theorem is referenced by:  sbceq1a 1934  a4sbc 1935  hbsbc1g 1938  hbsbcg 1941  sbccog 1942  sbcco2 1943  sbcng 1959  sbcimg 1960  sbcang 1961  sbcorg 1962  sbcbidig 1963  sbcalg 1964  sbcexg 1965  hbsbc1gd 1973  hbsbcgd 1974  ra4sbc 1987  csbeq1 1993  sbcco3g 2031  findes 3150  tfindes 3154  nn1suc 5887  uzindOLD 6156  nn0ind-raph 6162  seq1lem1 6246  uzind4s 6384  uzind4s2 6385  fzrevralt 6451  fzshftralt 6454

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-cleq 1462  df-clel 1465  df-sbc 1932

Copyright terms: Public domain