Metamath Proof Explorer

Theorem 2ralorOLD

Description: Obsolete version of 2ralor as of 20-Nov-2024. (Contributed by Jeff Madsen, 19-Jun-2010) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion 2ralorOLD ⊢∀x∈A∀y∈Bφ∨ψ↔∀x∈Aφ∨∀y∈Bψ

Proof

Step Hyp Ref Expression
1 rexnal ⊢∃x∈A¬φ↔¬∀x∈Aφ
2 rexnal ⊢∃y∈B¬ψ↔¬∀y∈Bψ
3 1 2 anbi12i ⊢∃x∈A¬φ∧∃y∈B¬ψ↔¬∀x∈Aφ∧¬∀y∈Bψ
4 ioran ⊢¬φ∨ψ↔¬φ∧¬ψ
5 4 rexbii ⊢∃y∈B¬φ∨ψ↔∃y∈B¬φ∧¬ψ
6 rexnal ⊢∃y∈B¬φ∨ψ↔¬∀y∈Bφ∨ψ
7 5 6 bitr3i ⊢∃y∈B¬φ∧¬ψ↔¬∀y∈Bφ∨ψ
8 7 rexbii ⊢∃x∈A∃y∈B¬φ∧¬ψ↔∃x∈A¬∀y∈Bφ∨ψ
9 reeanv ⊢∃x∈A∃y∈B¬φ∧¬ψ↔∃x∈A¬φ∧∃y∈B¬ψ
10 rexnal ⊢∃x∈A¬∀y∈Bφ∨ψ↔¬∀x∈A∀y∈Bφ∨ψ
11 8 9 10 3bitr3ri ⊢¬∀x∈A∀y∈Bφ∨ψ↔∃x∈A¬φ∧∃y∈B¬ψ
12 ioran ⊢¬∀x∈Aφ∨∀y∈Bψ↔¬∀x∈Aφ∧¬∀y∈Bψ
13 3 11 12 3bitr4i ⊢¬∀x∈A∀y∈Bφ∨ψ↔¬∀x∈Aφ∨∀y∈Bψ
14 13 con4bii ⊢∀x∈A∀y∈Bφ∨ψ↔∀x∈Aφ∨∀y∈Bψ