MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sb7f Structured version   Visualization version   GIF version

Theorem sb7f 2521
Description: This version of dfsb7 2251 does not require that 𝜑 and 𝑧 be distinct. This permits it to be used as a definition for substitution in a formalization that omits the logically redundant axiom ax-5 1888 i.e. that doesn't have the concept of a variable not occurring in a wff. (dfsb1 2464 is also suitable, but its mixing of free and bound variables is distasteful to some logicians.) (Contributed by NM, 26-Jul-2006.) (Revised by Mario Carneiro, 6-Oct-2016.)
Hypothesis
Ref Expression
sb7f.1 𝑧𝜑
Assertion
Ref Expression
sb7f ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧𝜑)))
Distinct variable group:   𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem sb7f
StepHypRef Expression
1 sb7f.1 . . . 4 𝑧𝜑
21sb5f 2492 . . 3 ([𝑧 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑧𝜑))
32sbbii 2054 . 2 ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑧]∃𝑥(𝑥 = 𝑧𝜑))
41sbco2 2507 . 2 ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
5 sb5 2240 . 2 ([𝑦 / 𝑧]∃𝑥(𝑥 = 𝑧𝜑) ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧𝜑)))
63, 4, 53bitr3i 302 1 ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396  wex 1761  wnf 1765  [wsb 2042
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043
This theorem is referenced by:  sb7h  2522  dfsb7OLDOLD  2523
  Copyright terms: Public domain W3C validator