Theorem raaan2 4463

Description: Rearrange restricted quantifiers with two different restricting classes, analogous to raaan 4459. 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

Step	Hyp	Ref	Expression
1		dfbi3 1044	. 2 ⊢ ((𝐴 = ∅ ↔ 𝐵 = ∅) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
2		rzal 4452	. . . . 5 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓))
3	2	adantr 483	. . . 4 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓))
4		rzal 4452	. . . . 5 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)
5	4	adantr 483	. . . 4 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → ∀𝑥 ∈ 𝐴 𝜑)
6		rzal 4452	. . . . 5 ⊢ (𝐵 = ∅ → ∀𝑦 ∈ 𝐵 𝜓)
7	6	adantl 484	. . . 4 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → ∀𝑦 ∈ 𝐵 𝜓)
8		pm5.1 821	. . . 4 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ∧ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
9	3, 5, 7, 8	syl12anc 834	. . 3 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
10		df-ne 3017	. . . . 5 ⊢ (𝐵 ≠ ∅ ↔ ¬ 𝐵 = ∅)
11		raaan2.1	. . . . . . 7 ⊢ Ⅎ𝑦𝜑
12	11	r19.28z 4442	. . . . . 6 ⊢ (𝐵 ≠ ∅ → (∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
13	12	ralbidv 3197	. . . . 5 ⊢ (𝐵 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
14	10, 13	sylbir 237	. . . 4 ⊢ (¬ 𝐵 = ∅ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
15		df-ne 3017	. . . . 5 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
16		nfcv 2977	. . . . . . 7 ⊢ Ⅎ𝑥𝐵
17		raaan2.2	. . . . . . 7 ⊢ Ⅎ𝑥𝜓
18	16, 17	nfralw 3225	. . . . . 6 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐵 𝜓
19	18	r19.27z 4449	. . . . 5 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
20	15, 19	sylbir 237	. . . 4 ⊢ (¬ 𝐴 = ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
21	14, 20	sylan9bbr 513	. . 3 ⊢ ((¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
22	9, 21	jaoi 853	. 2 ⊢ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
23	1, 22	sylbi 219	1 ⊢ ((𝐴 = ∅ ↔ 𝐵 = ∅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   = wceq 1533  Ⅎwnf 1780   ≠ wne 3016  ∀wral 3138  ∅c0 4290

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 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-dif 3938  df-nul 4291

This theorem is referenced by:  2reu4lem  4464