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

Theorem drsb1 2514
 Description: Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 2380. (Contributed by NM, 2-Jun-1993.) (New usage is discouraged.)
Assertion
Ref Expression
drsb1 (∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜑))

Proof of Theorem drsb1
StepHypRef Expression
1 equequ1 2033 . . . . 5 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
21sps 2183 . . . 4 (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
32imbi1d 346 . . 3 (∀𝑥 𝑥 = 𝑦 → ((𝑥 = 𝑧𝜑) ↔ (𝑦 = 𝑧𝜑)))
42anbi1d 633 . . . 4 (∀𝑥 𝑥 = 𝑦 → ((𝑥 = 𝑧𝜑) ↔ (𝑦 = 𝑧𝜑)))
54drex1 2453 . . 3 (∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑧𝜑) ↔ ∃𝑦(𝑦 = 𝑧𝜑)))
63, 5anbi12d 634 . 2 (∀𝑥 𝑥 = 𝑦 → (((𝑥 = 𝑧𝜑) ∧ ∃𝑥(𝑥 = 𝑧𝜑)) ↔ ((𝑦 = 𝑧𝜑) ∧ ∃𝑦(𝑦 = 𝑧𝜑))))
7 dfsb1 2500 . 2 ([𝑧 / 𝑥]𝜑 ↔ ((𝑥 = 𝑧𝜑) ∧ ∃𝑥(𝑥 = 𝑧𝜑)))
8 dfsb1 2500 . 2 ([𝑧 / 𝑦]𝜑 ↔ ((𝑦 = 𝑧𝜑) ∧ ∃𝑦(𝑦 = 𝑧𝜑)))
96, 7, 83bitr4g 318 1 (∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1537  ∃wex 1782  [wsb 2070 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-10 2143  ax-12 2176  ax-13 2380 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-ex 1783  df-nf 1787  df-sb 2071 This theorem is referenced by:  sb2ae  2515  sbco3  2533  iotaeq  6304
 Copyright terms: Public domain W3C validator
{"found_math": false, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0}