raaan2

Description: Rearrange restricted quantifiers with two different restricting classes, analogous to raaan . It is necessary that either both restricting classes are empty or both are not empty. (Contributed by Alexander van der Vekens, 29-Jun-2017)

	Ref	Expression
Hypotheses	raaan2.1	⊢ Ⅎ 𝑦 𝜑
	raaan2.2	⊢ Ⅎ 𝑥 𝜓
Assertion	raaan2	⊢ ( ( 𝐴 = ∅ ↔ 𝐵 = ∅ ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 𝜓 ) ) )

Proof

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

Metamath Proof Explorer

Theorem raaan2

Proof