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

Theorem mobiOLDOLD 2562
 Description: Obsolete proof of mobi 2560 as of 15-Oct-2022. (Contributed by BJ, 7-Oct-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
mobiOLDOLD (∀𝑥(𝜑𝜓) → (∃*𝑥𝜑 ↔ ∃*𝑥𝜓))

Proof of Theorem mobiOLDOLD
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 imbi1 339 . . . . . 6 ((𝜑𝜓) → ((𝜑𝑥 = 𝑦) ↔ (𝜓𝑥 = 𝑦)))
21alimi 1855 . . . . 5 (∀𝑥(𝜑𝜓) → ∀𝑥((𝜑𝑥 = 𝑦) ↔ (𝜓𝑥 = 𝑦)))
3 albi 1862 . . . . 5 (∀𝑥((𝜑𝑥 = 𝑦) ↔ (𝜓𝑥 = 𝑦)) → (∀𝑥(𝜑𝑥 = 𝑦) ↔ ∀𝑥(𝜓𝑥 = 𝑦)))
42, 3syl 17 . . . 4 (∀𝑥(𝜑𝜓) → (∀𝑥(𝜑𝑥 = 𝑦) ↔ ∀𝑥(𝜓𝑥 = 𝑦)))
54alrimiv 1970 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑦(∀𝑥(𝜑𝑥 = 𝑦) ↔ ∀𝑥(𝜓𝑥 = 𝑦)))
6 exbi 1891 . . 3 (∀𝑦(∀𝑥(𝜑𝑥 = 𝑦) ↔ ∀𝑥(𝜓𝑥 = 𝑦)) → (∃𝑦𝑥(𝜑𝑥 = 𝑦) ↔ ∃𝑦𝑥(𝜓𝑥 = 𝑦)))
75, 6syl 17 . 2 (∀𝑥(𝜑𝜓) → (∃𝑦𝑥(𝜑𝑥 = 𝑦) ↔ ∃𝑦𝑥(𝜓𝑥 = 𝑦)))
8 df-mo 2551 . 2 (∃*𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
9 df-mo 2551 . 2 (∃*𝑥𝜓 ↔ ∃𝑦𝑥(𝜓𝑥 = 𝑦))
107, 8, 93bitr4g 306 1 (∀𝑥(𝜑𝜓) → (∃*𝑥𝜑 ↔ ∃*𝑥𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198  ∀wal 1599  ∃wex 1823  ∃*wmo 2549 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953 This theorem depends on definitions:  df-bi 199  df-ex 1824  df-mo 2551 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator