Metamath Proof Explorer


Theorem 2ralor

Description: Distribute restricted universal quantification over "or". (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Assertion 2ralor ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝜓 ) ↔ ( ∀ 𝑥𝐴 𝜑 ∨ ∀ 𝑦𝐵 𝜓 ) )

Proof

Step Hyp Ref Expression
1 rexnal ( ∃ 𝑥𝐴 ¬ 𝜑 ↔ ¬ ∀ 𝑥𝐴 𝜑 )
2 rexnal ( ∃ 𝑦𝐵 ¬ 𝜓 ↔ ¬ ∀ 𝑦𝐵 𝜓 )
3 1 2 anbi12i ( ( ∃ 𝑥𝐴 ¬ 𝜑 ∧ ∃ 𝑦𝐵 ¬ 𝜓 ) ↔ ( ¬ ∀ 𝑥𝐴 𝜑 ∧ ¬ ∀ 𝑦𝐵 𝜓 ) )
4 ioran ( ¬ ( 𝜑𝜓 ) ↔ ( ¬ 𝜑 ∧ ¬ 𝜓 ) )
5 4 rexbii ( ∃ 𝑦𝐵 ¬ ( 𝜑𝜓 ) ↔ ∃ 𝑦𝐵 ( ¬ 𝜑 ∧ ¬ 𝜓 ) )
6 rexnal ( ∃ 𝑦𝐵 ¬ ( 𝜑𝜓 ) ↔ ¬ ∀ 𝑦𝐵 ( 𝜑𝜓 ) )
7 5 6 bitr3i ( ∃ 𝑦𝐵 ( ¬ 𝜑 ∧ ¬ 𝜓 ) ↔ ¬ ∀ 𝑦𝐵 ( 𝜑𝜓 ) )
8 7 rexbii ( ∃ 𝑥𝐴𝑦𝐵 ( ¬ 𝜑 ∧ ¬ 𝜓 ) ↔ ∃ 𝑥𝐴 ¬ ∀ 𝑦𝐵 ( 𝜑𝜓 ) )
9 reeanv ( ∃ 𝑥𝐴𝑦𝐵 ( ¬ 𝜑 ∧ ¬ 𝜓 ) ↔ ( ∃ 𝑥𝐴 ¬ 𝜑 ∧ ∃ 𝑦𝐵 ¬ 𝜓 ) )
10 rexnal ( ∃ 𝑥𝐴 ¬ ∀ 𝑦𝐵 ( 𝜑𝜓 ) ↔ ¬ ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝜓 ) )
11 8 9 10 3bitr3ri ( ¬ ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝜓 ) ↔ ( ∃ 𝑥𝐴 ¬ 𝜑 ∧ ∃ 𝑦𝐵 ¬ 𝜓 ) )
12 ioran ( ¬ ( ∀ 𝑥𝐴 𝜑 ∨ ∀ 𝑦𝐵 𝜓 ) ↔ ( ¬ ∀ 𝑥𝐴 𝜑 ∧ ¬ ∀ 𝑦𝐵 𝜓 ) )
13 3 11 12 3bitr4i ( ¬ ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝜓 ) ↔ ¬ ( ∀ 𝑥𝐴 𝜑 ∨ ∀ 𝑦𝐵 𝜓 ) )
14 13 con4bii ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝜓 ) ↔ ( ∀ 𝑥𝐴 𝜑 ∨ ∀ 𝑦𝐵 𝜓 ) )