Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  raaan2 Structured version   Visualization version   GIF version

Theorem raaan2 39733
Description: Rearrange restricted quantifiers with two different restricting classes, analogous to raaan 3935. It is necessary that either both restricting classes are empty or both are not empty. (Contributed by Alexander van der Vekens, 29-Jun-2017.)
Hypotheses
Ref Expression
raaan2.1 𝑦𝜑
raaan2.2 𝑥𝜓
Assertion
Ref Expression
raaan2 ((𝐴 = ∅ ↔ 𝐵 = ∅) → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem raaan2
StepHypRef Expression
1 dfbi3 932 . 2 ((𝐴 = ∅ ↔ 𝐵 = ∅) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
2 rzal 3928 . . . . 5 (𝐴 = ∅ → ∀𝑥𝐴𝑦𝐵 (𝜑𝜓))
32adantr 479 . . . 4 ((𝐴 = ∅ ∧ 𝐵 = ∅) → ∀𝑥𝐴𝑦𝐵 (𝜑𝜓))
4 rzal 3928 . . . . 5 (𝐴 = ∅ → ∀𝑥𝐴 𝜑)
54adantr 479 . . . 4 ((𝐴 = ∅ ∧ 𝐵 = ∅) → ∀𝑥𝐴 𝜑)
6 rzal 3928 . . . . 5 (𝐵 = ∅ → ∀𝑦𝐵 𝜓)
76adantl 480 . . . 4 ((𝐴 = ∅ ∧ 𝐵 = ∅) → ∀𝑦𝐵 𝜓)
8 pm5.1 897 . . . 4 ((∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ∧ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)) → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
93, 5, 7, 8syl12anc 1315 . . 3 ((𝐴 = ∅ ∧ 𝐵 = ∅) → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
10 df-ne 2686 . . . . 5 (𝐵 ≠ ∅ ↔ ¬ 𝐵 = ∅)
11 raaan2.1 . . . . . . 7 𝑦𝜑
1211r19.28z 3918 . . . . . 6 (𝐵 ≠ ∅ → (∀𝑦𝐵 (𝜑𝜓) ↔ (𝜑 ∧ ∀𝑦𝐵 𝜓)))
1312ralbidv 2873 . . . . 5 (𝐵 ≠ ∅ → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ ∀𝑥𝐴 (𝜑 ∧ ∀𝑦𝐵 𝜓)))
1410, 13sylbir 223 . . . 4 𝐵 = ∅ → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ ∀𝑥𝐴 (𝜑 ∧ ∀𝑦𝐵 𝜓)))
15 df-ne 2686 . . . . 5 (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
16 nfcv 2655 . . . . . . 7 𝑥𝐵
17 raaan2.2 . . . . . . 7 𝑥𝜓
1816, 17nfral 2833 . . . . . 6 𝑥𝑦𝐵 𝜓
1918r19.27z 3925 . . . . 5 (𝐴 ≠ ∅ → (∀𝑥𝐴 (𝜑 ∧ ∀𝑦𝐵 𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
2015, 19sylbir 223 . . . 4 𝐴 = ∅ → (∀𝑥𝐴 (𝜑 ∧ ∀𝑦𝐵 𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
2114, 20sylan9bbr 732 . . 3 ((¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅) → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
229, 21jaoi 392 . 2 (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)) → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
231, 22sylbi 205 1 ((𝐴 = ∅ ↔ 𝐵 = ∅) → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382   = wceq 1474  wnf 1698  wne 2684  wral 2800  c0 3777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-ral 2805  df-v 3079  df-dif 3447  df-nul 3778
This theorem is referenced by:  2reu4a  39747
  Copyright terms: Public domain W3C validator