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	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 ∨ 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∨ ∀ 𝑦 ∈ 𝐵 𝜓 ) )