This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ Ⅎ y φ
raaan2.2 ⊢ Ⅎ x ψ
Assertion raaan2 ⊢ A = ∅ ↔ B = ∅ → ∀ x ∈ A ∀ y ∈ B φ ∧ ψ ↔ ∀ x ∈ A φ ∧ ∀ y ∈ B ψ

Proof

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