Metamath Proof Explorer

Theorem r19.30OLD

Description: Obsolete version of r19.30 as of 18-Jun-2023. (Contributed by Scott Fenton, 25-Feb-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion r19.30OLD ⊢ ∀ x ∈ A φ ∨ ψ → ∀ x ∈ A φ ∨ ∃ x ∈ A ψ

Proof

Step Hyp Ref Expression
1 ralim ⊢ ∀ x ∈ A ¬ ψ → φ → ∀ x ∈ A ¬ ψ → ∀ x ∈ A φ
2 orcom ⊢ φ ∨ ψ ↔ ψ ∨ φ
3 df-or ⊢ ψ ∨ φ ↔ ¬ ψ → φ
4 2 3 bitri ⊢ φ ∨ ψ ↔ ¬ ψ → φ
5 4 ralbii ⊢ ∀ x ∈ A φ ∨ ψ ↔ ∀ x ∈ A ¬ ψ → φ
6 orcom ⊢ ∀ x ∈ A φ ∨ ¬ ∀ x ∈ A ¬ ψ ↔ ¬ ∀ x ∈ A ¬ ψ ∨ ∀ x ∈ A φ
7 dfrex2 ⊢ ∃ x ∈ A ψ ↔ ¬ ∀ x ∈ A ¬ ψ
8 7 orbi2i ⊢ ∀ x ∈ A φ ∨ ∃ x ∈ A ψ ↔ ∀ x ∈ A φ ∨ ¬ ∀ x ∈ A ¬ ψ
9 imor ⊢ ∀ x ∈ A ¬ ψ → ∀ x ∈ A φ ↔ ¬ ∀ x ∈ A ¬ ψ ∨ ∀ x ∈ A φ
10 6 8 9 3bitr4i ⊢ ∀ x ∈ A φ ∨ ∃ x ∈ A ψ ↔ ∀ x ∈ A ¬ ψ → ∀ x ∈ A φ
11 1 5 10 3imtr4i ⊢ ∀ x ∈ A φ ∨ ψ → ∀ x ∈ A φ ∨ ∃ x ∈ A ψ