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

Theorem r19.30 3063
 Description: Restricted quantifier version of 19.30 1798. (Contributed by Scott Fenton, 25-Feb-2011.)
Assertion
Ref Expression
r19.30 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ∨ ∃𝑥𝐴 𝜓))

Proof of Theorem r19.30
StepHypRef Expression
1 ralim 2932 . 2 (∀𝑥𝐴𝜓𝜑) → (∀𝑥𝐴 ¬ 𝜓 → ∀𝑥𝐴 𝜑))
2 orcom 401 . . . 4 ((𝜑𝜓) ↔ (𝜓𝜑))
3 df-or 384 . . . 4 ((𝜓𝜑) ↔ (¬ 𝜓𝜑))
42, 3bitri 263 . . 3 ((𝜑𝜓) ↔ (¬ 𝜓𝜑))
54ralbii 2963 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥𝐴𝜓𝜑))
6 orcom 401 . . 3 ((∀𝑥𝐴 𝜑 ∨ ¬ ∀𝑥𝐴 ¬ 𝜓) ↔ (¬ ∀𝑥𝐴 ¬ 𝜓 ∨ ∀𝑥𝐴 𝜑))
7 dfrex2 2979 . . . 4 (∃𝑥𝐴 𝜓 ↔ ¬ ∀𝑥𝐴 ¬ 𝜓)
87orbi2i 540 . . 3 ((∀𝑥𝐴 𝜑 ∨ ∃𝑥𝐴 𝜓) ↔ (∀𝑥𝐴 𝜑 ∨ ¬ ∀𝑥𝐴 ¬ 𝜓))
9 imor 427 . . 3 ((∀𝑥𝐴 ¬ 𝜓 → ∀𝑥𝐴 𝜑) ↔ (¬ ∀𝑥𝐴 ¬ 𝜓 ∨ ∀𝑥𝐴 𝜑))
106, 8, 93bitr4i 291 . 2 ((∀𝑥𝐴 𝜑 ∨ ∃𝑥𝐴 𝜓) ↔ (∀𝑥𝐴 ¬ 𝜓 → ∀𝑥𝐴 𝜑))
111, 5, 103imtr4i 280 1 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ∨ ∃𝑥𝐴 𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382  ∀wral 2896  ∃wrex 2897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902 This theorem is referenced by:  disjunsn  28789  esumcvg  29475
 Copyright terms: Public domain W3C validator