Metamath Proof Explorer


Theorem ralpr

Description: Convert a restricted universal quantification over a pair to a conjunction. (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 ralpr
|- ( A. 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 ralprg
 |-  ( ( A e. _V /\ B e. _V ) -> ( A. x e. { A , B } ph <-> ( ps /\ ch ) ) )
6 1 2 5 mp2an
 |-  ( A. x e. { A , B } ph <-> ( ps /\ ch ) )