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 ⊢Ⅎ_xB
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ψ