This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 19.44v

Description: Version of 19.44 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 12-Mar-1993)

Ref Expression
Assertion 19.44v ⊢ ∃ x φ ∨ ψ ↔ ∃ x φ ∨ ψ

Proof

Step Hyp Ref Expression
1 19.43 ⊢ ∃ x φ ∨ ψ ↔ ∃ x φ ∨ ∃ x ψ
2 19.9v ⊢ ∃ x ψ ↔ ψ
3 2 orbi2i ⊢ ∃ x φ ∨ ∃ x ψ ↔ ∃ x φ ∨ ψ
4 1 3 bitri ⊢ ∃ x φ ∨ ψ ↔ ∃ x φ ∨ ψ