NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  dfsbcq2 GIF version

Theorem dfsbcq2 3049
Description: This theorem, which is similar to Theorem 6.7 of [Quine] p. 42 and holds under both our definition and Quine's, relates logic substitution df-sb 1649 and substitution for class variables df-sbc 3047. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3048. (Contributed by NM, 31-Dec-2016.)
Assertion
Ref Expression
dfsbcq2 (y = A → ([y / x]φ ↔ [̣A / xφ))

Proof of Theorem dfsbcq2
StepHypRef Expression
1 eleq1 2413 . 2 (y = A → (y {x φ} ↔ A {x φ}))
2 df-clab 2340 . 2 (y {x φ} ↔ [y / x]φ)
3 df-sbc 3047 . . 3 ([̣A / xφA {x φ})
43bicomi 193 . 2 (A {x φ} ↔ [̣A / xφ)
51, 2, 43bitr3g 278 1 (y = A → ([y / x]φ ↔ [̣A / xφ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176   = wceq 1642  [wsb 1648   wcel 1710  {cab 2339  wsbc 3046
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-clab 2340  df-cleq 2346  df-clel 2349  df-sbc 3047
This theorem is referenced by:  sbsbc  3050  sbc8g  3053  sbc2or  3054  sbceq1a  3056  sbc5  3070  sbcng  3086  sbcimg  3087  sbcan  3088  sbcang  3089  sbcor  3090  sbcorg  3091  sbcbig  3092  sbcal  3093  sbcalg  3094  sbcex2  3095  sbcexg  3096  sbc3ang  3104  sbcel1gv  3105  sbcel2gv  3106  sbctt  3108  sbcralt  3118  sbcralg  3120  sbcrexg  3121  sbcreug  3122  rspsbc  3124  rspesbca  3126  sbcel12g  3151  sbceqg  3152  csbifg  3690  iota4  4357  csbiotag  4371  csbopabg  4637  sbcbrg  4685  opelopabsb  4697
  Copyright terms: Public domain W3C validator