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

Theorem ralprg 3825
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 3789 . . . 4  |-  { A ,  B }  =  ( { A }  u.  { B } )
21raleqi 2876 . . 3  |-  ( A. x  e.  { A ,  B } ph  <->  A. x  e.  ( { A }  u.  { B } )
ph )
3 ralunb 3496 . . 3  |-  ( A. x  e.  ( { A }  u.  { B } ) ph  <->  ( A. x  e.  { A } ph  /\  A. x  e.  { B } ph ) )
42, 3bitri 241 . 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 3814 . . 3  |-  ( A  e.  V  ->  ( A. x  e.  { A } ph  <->  ps ) )
7 ralprg.2 . . . 4  |-  ( x  =  B  ->  ( ph 
<->  ch ) )
87ralsng 3814 . . 3  |-  ( B  e.  W  ->  ( A. x  e.  { B } ph  <->  ch ) )
96, 8bi2anan9 844 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( ( A. x  e.  { A } ph  /\ 
A. x  e.  { B } ph )  <->  ( ps  /\ 
ch ) ) )
104, 9syl5bb 249 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 177    /\ wa 359    = wceq 1649    e. wcel 1721   A.wral 2674    u. cun 3286   {csn 3782   {cpr 3783
This theorem is referenced by:  raltpg  3827  ralpr  3829  iinxprg  4136  disjprg  4176  suppr  7437  injresinjlem  11162  gcdcllem2  12975  joinval2  14409  meetval2  14416  spwpr2  14623  iccntr  18813  limcun  19743  cusgra2v  21432  cusgra3v  21434  spthispth  21534  usgrcyclnl2  21589  4cycl4v4e  21614  4cycl4dv4e  21616  sumpr  24179  prsiga  24475  f12dfv  27969  f13dfv  27970  usgra2pthlem1  28048  usgra2pth  28049  frgra2v  28111  frgra3v  28114  3vfriswmgra  28117
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ral 2679  df-v 2926  df-sbc 3130  df-un 3293  df-sn 3788  df-pr 3789
  Copyright terms: Public domain W3C validator