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	|- A e. _V
	ralpr.2	|- B e. _V
	ralpr.3	|- ( x = A -> ( ph <-> ps ) )
	ralpr.4	|- ( x = B -> ( ph <-> ch ) )
Assertion	rexpr	|- ( E. x e. { A , B } ph <-> ( ps \/ ch ) )

Proof

Step	Hyp	Ref	Expression
1		ralpr.1	|- A e. _V
2		ralpr.2	|- B e. _V
3		ralpr.3	|- ( x = A -> ( ph <-> ps ) )
4		ralpr.4	|- ( x = B -> ( ph <-> ch ) )
5	3 4	rexprg	|- ( ( A e. _V /\ B e. _V ) -> ( E. x e. { A , B } ph <-> ( ps \/ ch ) ) )
6	1 2 5	mp2an	|- ( E. x e. { A , B } ph <-> ( ps \/ ch ) )