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

Theorem eeor 2335
Description: Distribute existential quantifiers. (Contributed by NM, 8-Aug-1994.) Avoid ax-10 2141. (Revised by GG, 21-Nov-2024.)
Hypotheses
Ref Expression
eeor.1 𝑦𝜑
eeor.2 𝑥𝜓
Assertion
Ref Expression
eeor (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑦𝜓))

Proof of Theorem eeor
StepHypRef Expression
1 19.43 1882 . . 3 (∃𝑦(𝜑𝜓) ↔ (∃𝑦𝜑 ∨ ∃𝑦𝜓))
21exbii 1848 . 2 (∃𝑥𝑦(𝜑𝜓) ↔ ∃𝑥(∃𝑦𝜑 ∨ ∃𝑦𝜓))
3 19.43 1882 . . 3 (∃𝑥(∃𝑦𝜑 ∨ ∃𝑦𝜓) ↔ (∃𝑥𝑦𝜑 ∨ ∃𝑥𝑦𝜓))
4 eeor.1 . . . . . 6 𝑦𝜑
5419.9 2205 . . . . 5 (∃𝑦𝜑𝜑)
65exbii 1848 . . . 4 (∃𝑥𝑦𝜑 ↔ ∃𝑥𝜑)
7 excom 2162 . . . . 5 (∃𝑥𝑦𝜓 ↔ ∃𝑦𝑥𝜓)
8 eeor.2 . . . . . . 7 𝑥𝜓
9819.9 2205 . . . . . 6 (∃𝑥𝜓𝜓)
109exbii 1848 . . . . 5 (∃𝑦𝑥𝜓 ↔ ∃𝑦𝜓)
117, 10bitri 275 . . . 4 (∃𝑥𝑦𝜓 ↔ ∃𝑦𝜓)
126, 11orbi12i 915 . . 3 ((∃𝑥𝑦𝜑 ∨ ∃𝑥𝑦𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑦𝜓))
133, 12bitri 275 . 2 (∃𝑥(∃𝑦𝜑 ∨ ∃𝑦𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑦𝜓))
142, 13bitri 275 1 (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑦𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wo 848  wex 1779  wnf 1783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-11 2157  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-or 849  df-ex 1780  df-nf 1784
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator