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

Theorem raaan2 4516
Description: Rearrange restricted quantifiers with two different restricting classes, analogous to raaan 4512. 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 1046 . 2 ((𝐴 = ∅ ↔ 𝐵 = ∅) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
2 rzal 4500 . . . . 5 (𝐴 = ∅ → ∀𝑥𝐴𝑦𝐵 (𝜑𝜓))
32adantr 480 . . . 4 ((𝐴 = ∅ ∧ 𝐵 = ∅) → ∀𝑥𝐴𝑦𝐵 (𝜑𝜓))
4 rzal 4500 . . . . 5 (𝐴 = ∅ → ∀𝑥𝐴 𝜑)
54adantr 480 . . . 4 ((𝐴 = ∅ ∧ 𝐵 = ∅) → ∀𝑥𝐴 𝜑)
6 rzal 4500 . . . . 5 (𝐵 = ∅ → ∀𝑦𝐵 𝜓)
76adantl 481 . . . 4 ((𝐴 = ∅ ∧ 𝐵 = ∅) → ∀𝑦𝐵 𝜓)
8 pm5.1 821 . . . 4 ((∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ∧ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)) → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
93, 5, 7, 8syl12anc 834 . . 3 ((𝐴 = ∅ ∧ 𝐵 = ∅) → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
10 df-ne 2933 . . . . 5 (𝐵 ≠ ∅ ↔ ¬ 𝐵 = ∅)
11 raaan2.1 . . . . . . 7 𝑦𝜑
1211r19.28z 4489 . . . . . 6 (𝐵 ≠ ∅ → (∀𝑦𝐵 (𝜑𝜓) ↔ (𝜑 ∧ ∀𝑦𝐵 𝜓)))
1312ralbidv 3169 . . . . 5 (𝐵 ≠ ∅ → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ ∀𝑥𝐴 (𝜑 ∧ ∀𝑦𝐵 𝜓)))
1410, 13sylbir 234 . . . 4 𝐵 = ∅ → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ ∀𝑥𝐴 (𝜑 ∧ ∀𝑦𝐵 𝜓)))
15 df-ne 2933 . . . . 5 (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
16 nfcv 2895 . . . . . . 7 𝑥𝐵
17 raaan2.2 . . . . . . 7 𝑥𝜓
1816, 17nfralw 3300 . . . . . 6 𝑥𝑦𝐵 𝜓
1918r19.27z 4496 . . . . 5 (𝐴 ≠ ∅ → (∀𝑥𝐴 (𝜑 ∧ ∀𝑦𝐵 𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
2015, 19sylbir 234 . . . 4 𝐴 = ∅ → (∀𝑥𝐴 (𝜑 ∧ ∀𝑦𝐵 𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
2114, 20sylan9bbr 510 . . 3 ((¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅) → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
229, 21jaoi 854 . 2 (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)) → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
231, 22sylbi 216 1 ((𝐴 = ∅ ↔ 𝐵 = ∅) → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 844   = wceq 1533  wnf 1777  wne 2932  wral 3053  c0 4314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-dif 3943  df-nul 4315
This theorem is referenced by:  2reu4lem  4517
  Copyright terms: Public domain W3C validator