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

Theorem cbvalvOLD 2375
 Description: Obsolete version of cbvalv 2373 as of 11-Sep-2023. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2111. (Revised by Wolf Lammen, 17-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
cbvalv.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvalvOLD (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Distinct variable groups:   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvalvOLD
StepHypRef Expression
1 ax-5 1889 . . . 4 (𝜑 → ∀𝑦𝜑)
21hbal 2137 . . 3 (∀𝑥𝜑 → ∀𝑦𝑥𝜑)
3 cbvalv.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
43spv 2366 . . 3 (∀𝑥𝜑𝜓)
52, 4alrimih 1806 . 2 (∀𝑥𝜑 → ∀𝑦𝜓)
6 ax-5 1889 . . . 4 (𝜓 → ∀𝑥𝜓)
76hbal 2137 . . 3 (∀𝑦𝜓 → ∀𝑥𝑦𝜓)
83equcoms 2005 . . . . 5 (𝑦 = 𝑥 → (𝜑𝜓))
98bicomd 224 . . . 4 (𝑦 = 𝑥 → (𝜓𝜑))
109spv 2366 . . 3 (∀𝑦𝜓𝜑)
117, 10alrimih 1806 . 2 (∀𝑦𝜓 → ∀𝑥𝜑)
125, 11impbii 210 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1520 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-11 2125  ax-12 2140  ax-13 2343 This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1763  df-nf 1767 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator