 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 31809
 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 2417 which is valid for disjoint variables, so we introduce a dummy variable 𝑦 to isolate 𝑥 from 𝑡, as in dfsb7 2443 with respect to sb5 2418. 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 DV condition on the substitute and the substituted variables, and then prove the original theorem by applying this lemma twice in a row. A drawback compared with df-sb 1868 is that this definition uses a dummy variable and therefore requires a justification theorem, which requires some of the auxiliary axiom schemes. 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 2041, of the substitution axiom ax-12 2034, and of commutation of quantifiers ax-11 2021; that is, ax-13 2234 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 31808 . 2 wff [𝑡/𝑥]b𝜑
5 vy . . . . 5 setvar 𝑦
65, 3weq 1861 . . . 4 wff 𝑦 = 𝑡
72, 5weq 1861 . . . . . 6 wff 𝑥 = 𝑦
87, 1wi 4 . . . . 5 wff (𝑥 = 𝑦𝜑)
98, 2wal 1473 . . . 4 wff 𝑥(𝑥 = 𝑦𝜑)
106, 9wi 4 . . 3 wff (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑))
1110, 5wal 1473 . 2 wff 𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑))
124, 11wb 195 1 wff ([𝑡/𝑥]b𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)))
 Colors of variables: wff setvar class This definition is referenced by:  bj-ssbim  31810  bj-alsb  31814  bj-sbex  31815  bj-ssbeq  31816  bj-ssb0  31817  bj-ssbequ  31818  bj-ssb1a  31821  bj-ssb1  31822  bj-dfssb2  31829  bj-ssbn  31830  bj-ssbequ2  31832  bj-ssbequ1  31833  bj-ssbid2ALT  31835  bj-ssbid1ALT  31837  bj-ssbssblem  31838
 Copyright terms: Public domain W3C validator