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

Theorem raaan2 4527
Description: Rearrange restricted quantifiers with two different restricting classes, analogous to raaan 4523. 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 1049 . 2 ((𝐴 = ∅ ↔ 𝐵 = ∅) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
2 rzal 4515 . . . . 5 (𝐴 = ∅ → ∀𝑥𝐴𝑦𝐵 (𝜑𝜓))
32adantr 480 . . . 4 ((𝐴 = ∅ ∧ 𝐵 = ∅) → ∀𝑥𝐴𝑦𝐵 (𝜑𝜓))
4 rzal 4515 . . . . 5 (𝐴 = ∅ → ∀𝑥𝐴 𝜑)
54adantr 480 . . . 4 ((𝐴 = ∅ ∧ 𝐵 = ∅) → ∀𝑥𝐴 𝜑)
6 rzal 4515 . . . . 5 (𝐵 = ∅ → ∀𝑦𝐵 𝜓)
76adantl 481 . . . 4 ((𝐴 = ∅ ∧ 𝐵 = ∅) → ∀𝑦𝐵 𝜓)
8 pm5.1 824 . . . 4 ((∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ∧ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)) → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
93, 5, 7, 8syl12anc 837 . . 3 ((𝐴 = ∅ ∧ 𝐵 = ∅) → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
10 df-ne 2939 . . . . 5 (𝐵 ≠ ∅ ↔ ¬ 𝐵 = ∅)
11 raaan2.1 . . . . . . 7 𝑦𝜑
1211r19.28z 4504 . . . . . 6 (𝐵 ≠ ∅ → (∀𝑦𝐵 (𝜑𝜓) ↔ (𝜑 ∧ ∀𝑦𝐵 𝜓)))
1312ralbidv 3176 . . . . 5 (𝐵 ≠ ∅ → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ ∀𝑥𝐴 (𝜑 ∧ ∀𝑦𝐵 𝜓)))
1410, 13sylbir 235 . . . 4 𝐵 = ∅ → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ ∀𝑥𝐴 (𝜑 ∧ ∀𝑦𝐵 𝜓)))
15 df-ne 2939 . . . . 5 (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
16 nfcv 2903 . . . . . . 7 𝑥𝐵
17 raaan2.2 . . . . . . 7 𝑥𝜓
1816, 17nfralw 3309 . . . . . 6 𝑥𝑦𝐵 𝜓
1918r19.27z 4511 . . . . 5 (𝐴 ≠ ∅ → (∀𝑥𝐴 (𝜑 ∧ ∀𝑦𝐵 𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
2015, 19sylbir 235 . . . 4 𝐴 = ∅ → (∀𝑥𝐴 (𝜑 ∧ ∀𝑦𝐵 𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
2114, 20sylan9bbr 510 . . 3 ((¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅) → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
229, 21jaoi 857 . 2 (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)) → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
231, 22sylbi 217 1 ((𝐴 = ∅ ↔ 𝐵 = ∅) → (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑦𝐵 𝜓)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847   = wceq 1537  wnf 1780  wne 2938  wral 3059  c0 4339
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-dif 3966  df-nul 4340
This theorem is referenced by:  2reu4lem  4528
  Copyright terms: Public domain W3C validator