Theorem dfsbcq 1988

Description: This theorem, which is similar to Theorem 6.7 of [Quine] p. 42, provides us with a weak definition of the proper substitution of a class for a set, which we will use in place of df-sbc 1987 above. We will derive all our results from starting from here instead of df-sbc 1987. As a consequence, we can derive elabs 2014, which is a weaker version of df-sbc 1987 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 2001 assertion (always false) or as in sbc6 2002 (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 definition has neither behavior for proper classes, and by using dfsbcq 1988 as the definition, we leave it unspecified so as not to conflict. Quine's definition is based on the formula's structure rather than its logical properties and apparently cannot be expressed directly in our formal system.)

While in principle we could have made this theorem the official definition, we use df-sbc 1987 because it is more obviously eliminable and thus easier to justify metalogically. But to avoid conflict with Quine, we never use df-sbc 1987 except indirectly via this theorem.

Assertion

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

Proof of Theorem dfsbcq

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

Syntax hints:   -> wi 3   <-> wb 144   = wceq 992   e. wcel 994  [wsbc 1207  {cab 1505

This theorem is referenced by:  sbceq1a 1989  a4sbc 1990  hbsbc1g 1993  hbsbcg 1996  sbccog 1997  sbcco2 1998  sbcng 2017  sbcimg 2018  sbcang 2019  sbcorg 2020  sbcbidig 2021  sbcalg 2022  sbcexg 2023  hbsbc1gd 2031  hbsbcgd 2032  ra4sbc 2047  csbeq1 2053  sbcco3g 2093  tfindes 3215  findes 3248  nn1suc 6084  uzindOLD 6379  nn0ind-raph 6385  uzind4s 6579  uzind4s2 6580  fzrevral 6650  fzshftral 6653  subtr2 11396  cbvsbc 11398  morex 11804  ac6gf 11841  sdc 11877

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-cleq 1511  df-clel 1514  df-sbc 1987

Copyright terms: Public domain