MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralpr Structured version   Unicode version

Theorem ralpr 4040
Description: Convert a quantification over a pair to a conjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
Hypotheses
Ref Expression
ralpr.1  |-  A  e. 
_V
ralpr.2  |-  B  e. 
_V
ralpr.3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
ralpr.4  |-  ( x  =  B  ->  ( ph 
<->  ch ) )
Assertion
Ref Expression
ralpr  |-  ( A. x  e.  { A ,  B } ph  <->  ( ps  /\ 
ch ) )
Distinct variable groups:    x, A    x, B    ps, x    ch, x
Allowed substitution hint:    ph( x)

Proof of Theorem ralpr
StepHypRef Expression
1 ralpr.1 . 2  |-  A  e. 
_V
2 ralpr.2 . 2  |-  B  e. 
_V
3 ralpr.3 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
4 ralpr.4 . . 3  |-  ( x  =  B  ->  ( ph 
<->  ch ) )
53, 4ralprg 4036 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A. x  e. 
{ A ,  B } ph  <->  ( ps  /\  ch ) ) )
61, 2, 5mp2an 672 1  |-  ( A. x  e.  { A ,  B } ph  <->  ( ps  /\ 
ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1370    e. wcel 1758   A.wral 2799   _Vcvv 3078   {cpr 3990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2804  df-v 3080  df-sbc 3295  df-un 3444  df-sn 3989  df-pr 3991
This theorem is referenced by:  fzprval  11638  xpsfrnel  14624  xpsle  14642  isdrs2  15232  pmtrsn  16148  iblcnlem1  21408  wlkntrllem2  23638  wlkntrllem3  23639  2wlklem  23642  subfacp1lem3  27237  fprb  27751  usgra2pthspth  30466  usgra2wlkspthlem1  30467  numclwwlkovf2ex  30850  ldepsnlinc  31205
  Copyright terms: Public domain W3C validator