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

Metamath Proof Explorer

Theorem rexpr

Description: Convert a restricted existential quantification over a pair to a disjunction. (Contributed by NM, 3-Jun-2007) (Revised by Mario Carneiro, 23-Apr-2015)

	Ref	Expression
Hypotheses	ralpr.1	⊢ 𝐴 ∈ V
	ralpr.2	⊢ 𝐵 ∈ V
	ralpr.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	ralpr.4	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜒 ) )
Assertion	rexpr	⊢ ( ∃ 𝑥 ∈ { 𝐴 , 𝐵 } 𝜑 ↔ ( 𝜓 ∨ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		ralpr.1	⊢ 𝐴 ∈ V
2		ralpr.2	⊢ 𝐵 ∈ V
3		ralpr.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
4		ralpr.4	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜒 ) )
5	3 4	rexprg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ∃ 𝑥 ∈ { 𝐴 , 𝐵 } 𝜑 ↔ ( 𝜓 ∨ 𝜒 ) ) )
6	1 2 5	mp2an	⊢ ( ∃ 𝑥 ∈ { 𝐴 , 𝐵 } 𝜑 ↔ ( 𝜓 ∨ 𝜒 ) )