Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ssb Structured version   Visualization version   GIF version

Definition df-ssb 32989
Description: Alternate definition of proper substitution. Note that the occurrences of a given variable are either all bound (𝑥, 𝑦) or all free (𝑡). Also note that the definiens uses only primitive symbols. It is obtained by applying twice Tarski's definition sb6 2285 which is valid for disjoint variables, so we introduce a dummy variable 𝑦 to isolate 𝑥 from 𝑡, as in dfsb7 2547 with respect to sb5 2286.

This double level definition will make several proofs using it appear as doubled. Alternately, one could often first prove as a lemma the same theorem with a disjoint variable condition on the substitute and the substituted variables, and then prove the original theorem by applying this lemma twice in a row.

This definition uses a dummy variable, but the justification theorem, bj-ssbjust 32987, is provable from Tarski's FOL.

Once this is proved, more of the fundamental properties of proper substitution will be provable from Tarski's FOL system, sometimes with the help of specialization sp 2215, of the substitution axiom ax-12 2211, and of commutation of quantifiers ax-11 2198; that is, ax-13 2352 will often be avoided. (Contributed by BJ, 22-Dec-2020.)

Assertion
Ref Expression
df-ssb ([𝑡/𝑥]b𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)))
Distinct variable groups:   𝑥,𝑦   𝑦,𝑡   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑡)

Detailed syntax breakdown of Definition df-ssb
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 vt . . 3 setvar 𝑡
41, 2, 3wssb 32988 . 2 wff [𝑡/𝑥]b𝜑
5 vy . . . . 5 setvar 𝑦
65, 3weq 2055 . . . 4 wff 𝑦 = 𝑡
72, 5weq 2055 . . . . . 6 wff 𝑥 = 𝑦
87, 1wi 4 . . . . 5 wff (𝑥 = 𝑦𝜑)
98, 2wal 1650 . . . 4 wff 𝑥(𝑥 = 𝑦𝜑)
106, 9wi 4 . . 3 wff (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑))
1110, 5wal 1650 . 2 wff 𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑))
124, 11wb 197 1 wff ([𝑡/𝑥]b𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)))
Colors of variables: wff setvar class
This definition is referenced by:  bj-ssbim  32990  bj-alsb  32994  bj-sbex  32995  bj-ssbeq  32996  bj-ssb0  32997  bj-ssbequ  32998  bj-ssb1a  33001  bj-ssb1  33002  bj-dfssb2  33008  bj-ssbn  33009  bj-ssbequ2  33011  bj-ssbequ1  33012  bj-ssbid2ALT  33014  bj-ssbid1ALT  33016  bj-ssbssblem  33017
  Copyright terms: Public domain W3C validator