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

Theorem sbralie 3356
Description: Implicit to explicit substitution that swaps variables in a rectrictedly universally quantified expression. (Contributed by NM, 5-Sep-2004.) Avoid ax-ext 2706, df-cleq 2727, df-clel 2814. (Revised by Wolf Lammen, 10-Mar-2025.)
Hypothesis
Ref Expression
sbralie.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
sbralie (∀𝑥𝑦 𝜑 ↔ [𝑦 / 𝑥]∀𝑦𝑥 𝜓)
Distinct variable groups:   𝑥,𝑦   𝜓,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem sbralie
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-ral 3060 . 2 (∀𝑥𝑦 𝜑 ↔ ∀𝑥(𝑥𝑦𝜑))
2 nfv 1912 . . . . 5 𝑧𝜑
32sblim 2305 . . . 4 ([𝑦 / 𝑧](𝑥𝑧𝜑) ↔ ([𝑦 / 𝑧]𝑥𝑧𝜑))
4 elsb2 2123 . . . . 5 ([𝑦 / 𝑧]𝑥𝑧𝑥𝑦)
54imbi1i 349 . . . 4 (([𝑦 / 𝑧]𝑥𝑧𝜑) ↔ (𝑥𝑦𝜑))
63, 5bitri 275 . . 3 ([𝑦 / 𝑧](𝑥𝑧𝜑) ↔ (𝑥𝑦𝜑))
76albii 1816 . 2 (∀𝑥[𝑦 / 𝑧](𝑥𝑧𝜑) ↔ ∀𝑥(𝑥𝑦𝜑))
8 elequ1 2113 . . . . . . 7 (𝑥 = 𝑦 → (𝑥𝑧𝑦𝑧))
9 sbralie.1 . . . . . . 7 (𝑥 = 𝑦 → (𝜑𝜓))
108, 9imbi12d 344 . . . . . 6 (𝑥 = 𝑦 → ((𝑥𝑧𝜑) ↔ (𝑦𝑧𝜓)))
1110cbvalvw 2033 . . . . 5 (∀𝑥(𝑥𝑧𝜑) ↔ ∀𝑦(𝑦𝑧𝜓))
12 df-ral 3060 . . . . . . 7 (∀𝑦𝑥 𝜓 ↔ ∀𝑦(𝑦𝑥𝜓))
1312sbbii 2074 . . . . . 6 ([𝑧 / 𝑥]∀𝑦𝑥 𝜓 ↔ [𝑧 / 𝑥]∀𝑦(𝑦𝑥𝜓))
14 sbal 2167 . . . . . 6 ([𝑧 / 𝑥]∀𝑦(𝑦𝑥𝜓) ↔ ∀𝑦[𝑧 / 𝑥](𝑦𝑥𝜓))
15 nfv 1912 . . . . . . . . 9 𝑥𝜓
1615sblim 2305 . . . . . . . 8 ([𝑧 / 𝑥](𝑦𝑥𝜓) ↔ ([𝑧 / 𝑥]𝑦𝑥𝜓))
17 elsb2 2123 . . . . . . . . 9 ([𝑧 / 𝑥]𝑦𝑥𝑦𝑧)
1817imbi1i 349 . . . . . . . 8 (([𝑧 / 𝑥]𝑦𝑥𝜓) ↔ (𝑦𝑧𝜓))
1916, 18bitri 275 . . . . . . 7 ([𝑧 / 𝑥](𝑦𝑥𝜓) ↔ (𝑦𝑧𝜓))
2019albii 1816 . . . . . 6 (∀𝑦[𝑧 / 𝑥](𝑦𝑥𝜓) ↔ ∀𝑦(𝑦𝑧𝜓))
2113, 14, 203bitrri 298 . . . . 5 (∀𝑦(𝑦𝑧𝜓) ↔ [𝑧 / 𝑥]∀𝑦𝑥 𝜓)
2211, 21bitri 275 . . . 4 (∀𝑥(𝑥𝑧𝜑) ↔ [𝑧 / 𝑥]∀𝑦𝑥 𝜓)
2322sbbii 2074 . . 3 ([𝑦 / 𝑧]∀𝑥(𝑥𝑧𝜑) ↔ [𝑦 / 𝑧][𝑧 / 𝑥]∀𝑦𝑥 𝜓)
24 sbal 2167 . . 3 ([𝑦 / 𝑧]∀𝑥(𝑥𝑧𝜑) ↔ ∀𝑥[𝑦 / 𝑧](𝑥𝑧𝜑))
25 sbco2vv 2097 . . 3 ([𝑦 / 𝑧][𝑧 / 𝑥]∀𝑦𝑥 𝜓 ↔ [𝑦 / 𝑥]∀𝑦𝑥 𝜓)
2623, 24, 253bitr3i 301 . 2 (∀𝑥[𝑦 / 𝑧](𝑥𝑧𝜑) ↔ [𝑦 / 𝑥]∀𝑦𝑥 𝜓)
271, 7, 263bitr2i 299 1 (∀𝑥𝑦 𝜑 ↔ [𝑦 / 𝑥]∀𝑦𝑥 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1535  [wsb 2062  wral 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-nf 1781  df-sb 2063  df-ral 3060
This theorem is referenced by:  tfinds2  7885
  Copyright terms: Public domain W3C validator