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

Metamath Proof Explorer

Theorem 3r19.43

Description: Restricted quantifier version of 19.43 for a triple disjunction . (Contributed by AV, 2-Nov-2025)

Ref Expression
Assertion 3r19.43 ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ∨ ∃ 𝑥 ∈ 𝐴 𝜒 ) )

Proof

Step Hyp Ref Expression
1 df-3or ⊢ ( ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) )
2 1 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) ↔ ∃ 𝑥 ∈ 𝐴 ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) )
3 r19.43 ⊢ ( ∃ 𝑥 ∈ 𝐴 ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) ∨ ∃ 𝑥 ∈ 𝐴 𝜒 ) )
4 r19.43 ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) )
5 4 orbi1i ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) ∨ ∃ 𝑥 ∈ 𝐴 𝜒 ) ↔ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) ∨ ∃ 𝑥 ∈ 𝐴 𝜒 ) )
6 df-3or ⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ∨ ∃ 𝑥 ∈ 𝐴 𝜒 ) ↔ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) ∨ ∃ 𝑥 ∈ 𝐴 𝜒 ) )
7 5 6 bitr4i ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) ∨ ∃ 𝑥 ∈ 𝐴 𝜒 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ∨ ∃ 𝑥 ∈ 𝐴 𝜒 ) )
8 2 3 7 3bitri ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ∨ ∃ 𝑥 ∈ 𝐴 𝜒 ) )