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	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ∨ ∃ 𝑥 ∈ 𝐴 𝜒 ) )