Theorem raaan2 4477

Description: Rearrange restricted quantifiers with two different restricting classes, analogous to raaan 4473. 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 4449	. . . . 5 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓))
3	2	adantr 486	. . . 4 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓))
4		rzal 4449	. . . . 5 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)
5	4	adantr 486	. . . 4 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → ∀𝑥 ∈ 𝐴 𝜑)
6		rzal 4449	. . . . 5 ⊢ (𝐵 = ∅ → ∀𝑦 ∈ 𝐵 𝜓)
7	6	adantl 487	. . . 4 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → ∀𝑦 ∈ 𝐵 𝜓)
8		pm5.1 836	. . . 4 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ∧ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
9	3, 5, 7, 8	syl12anc 850	. . 3 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
10		df-ne 2956	. . . . 5 ⊢ (𝐵 ≠ ∅ ↔ ¬ 𝐵 = ∅)
11		raaan2.1	. . . . . . 7 ⊢ Ⅎ𝑦𝜑
12	11	r19.28z 4457	. . . . . 6 ⊢ (𝐵 ≠ ∅ → (∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
13	12	ralbidv 3185	. . . . 5 ⊢ (𝐵 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
14	10, 13	sylbir 238	. . . 4 ⊢ (¬ 𝐵 = ∅ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
15		df-ne 2956	. . . . 5 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
16		nfcv 2922	. . . . . . 7 ⊢ Ⅎ𝑥𝐵
17		raaan2.2	. . . . . . 7 ⊢ Ⅎ𝑥𝜓
18	16, 17	nfralw 3309	. . . . . 6 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐵 𝜓
19	18	r19.27z 4465	. . . . 5 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
20	15, 19	sylbir 238	. . . 4 ⊢ (¬ 𝐴 = ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
21	14, 20	sylan9bbr 520	. . 3 ⊢ ((¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
22	9, 21	jaoi 871	. 2 ⊢ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
23	1, 22	sylbi 220	1 ⊢ ((𝐴 = ∅ ↔ 𝐵 = ∅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1569  Ⅎwnf 1815   ≠ wne 2955  ∀wral 3076  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-dif 4047  df-nul 4279

This theorem is used by:  2reu4lem  4478