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

Theorem ralprg 3758
Description: Convert a quantification over a pair to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
Hypotheses
Ref Expression
ralprg.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
ralprg.2  |-  ( x  =  B  ->  ( ph 
<->  ch ) )
Assertion
Ref Expression
ralprg  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A. x  e. 
{ A ,  B } ph  <->  ( ps  /\  ch ) ) )
Distinct variable groups:    x, A    x, B    ps, x    ch, x
Allowed substitution hints:    ph( x)    V( x)    W( x)

Proof of Theorem ralprg
StepHypRef Expression
1 df-pr 3723 . . . 4  |-  { A ,  B }  =  ( { A }  u.  { B } )
21raleqi 2816 . . 3  |-  ( A. x  e.  { A ,  B } ph  <->  A. x  e.  ( { A }  u.  { B } )
ph )
3 ralunb 3432 . . 3  |-  ( A. x  e.  ( { A }  u.  { B } ) ph  <->  ( A. x  e.  { A } ph  /\  A. x  e.  { B } ph ) )
42, 3bitri 240 . 2  |-  ( A. x  e.  { A ,  B } ph  <->  ( A. x  e.  { A } ph  /\  A. x  e.  { B } ph ) )
5 ralprg.1 . . . 4  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
65ralsng 3748 . . 3  |-  ( A  e.  V  ->  ( A. x  e.  { A } ph  <->  ps ) )
7 ralprg.2 . . . 4  |-  ( x  =  B  ->  ( ph 
<->  ch ) )
87ralsng 3748 . . 3  |-  ( B  e.  W  ->  ( A. x  e.  { B } ph  <->  ch ) )
96, 8bi2anan9 843 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( ( A. x  e.  { A } ph  /\ 
A. x  e.  { B } ph )  <->  ( ps  /\ 
ch ) ) )
104, 9syl5bb 248 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A. x  e. 
{ A ,  B } ph  <->  ( ps  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1642    e. wcel 1710   A.wral 2619    u. cun 3226   {csn 3716   {cpr 3717
This theorem is referenced by:  raltpg  3760  ralpr  3762  iinxprg  4058  disjprg  4098  suppr  7306  gcdcllem2  12782  joinval2  14216  meetval2  14223  spwpr2  14430  iccntr  18423  limcun  19343  sumpr  23410  prsiga  23780  injresinjlem  27459  cusgra2v  27617  cusgra3v  27619  wlkntrllem4  27687  wlkntrllem5  27688  spthispth  27698  usgrcyclnl2  27748  4cycl4v4e  27773  4cycl4dv4e  27775  frgra2v  27815  frgra3v  27818  3vfriswmgra  27821
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ral 2624  df-v 2866  df-sbc 3068  df-un 3233  df-sn 3722  df-pr 3723
  Copyright terms: Public domain W3C validator