Theorem raaan2 4483

Description: Rearrange restricted quantifiers with two different restricting classes, analogous to raaan 4479. 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 1065	. 2 ⊢ ((𝐴 = ∅ ↔ 𝐵 = ∅) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
2		rzal 4455	. . . . 5 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓))
3	2	adantr 485	. . . 4 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓))
4		rzal 4455	. . . . 5 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)
5	4	adantr 485	. . . 4 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → ∀𝑥 ∈ 𝐴 𝜑)
6		rzal 4455	. . . . 5 ⊢ (𝐵 = ∅ → ∀𝑦 ∈ 𝐵 𝜓)
7	6	adantl 486	. . . 4 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → ∀𝑦 ∈ 𝐵 𝜓)
8		pm5.1 835	. . . 4 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ∧ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
9	3, 5, 7, 8	syl12anc 849	. . 3 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
10		df-ne 2959	. . . . 5 ⊢ (𝐵 ≠ ∅ ↔ ¬ 𝐵 = ∅)
11		raaan2.1	. . . . . . 7 ⊢ Ⅎ𝑦𝜑
12	11	r19.28z 4463	. . . . . 6 ⊢ (𝐵 ≠ ∅ → (∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
13	12	ralbidv 3188	. . . . 5 ⊢ (𝐵 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
14	10, 13	sylbir 238	. . . 4 ⊢ (¬ 𝐵 = ∅ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
15		df-ne 2959	. . . . 5 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
16		nfcv 2925	. . . . . . 7 ⊢ Ⅎ𝑥𝐵
17		raaan2.2	. . . . . . 7 ⊢ Ⅎ𝑥𝜓
18	16, 17	nfralw 3312	. . . . . 6 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐵 𝜓
19	18	r19.27z 4471	. . . . 5 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
20	15, 19	sylbir 238	. . . 4 ⊢ (¬ 𝐴 = ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
21	14, 20	sylan9bbr 519	. . 3 ⊢ ((¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
22	9, 21	jaoi 870	. 2 ⊢ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
23	1, 22	sylbi 220	1 ⊢ ((𝐴 = ∅ ↔ 𝐵 = ∅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   = wceq 1570  Ⅎwnf 1813   ≠ wne 2958  ∀wral 3079  ∅c0 4286

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-dif 3908  df-nul 4287

This theorem is used by:  2reu4lem  4484