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

Theorem ralprg 3817
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 3781 . . . 4  |-  { A ,  B }  =  ( { A }  u.  { B } )
21raleqi 2868 . . 3  |-  ( A. x  e.  { A ,  B } ph  <->  A. x  e.  ( { A }  u.  { B } )
ph )
3 ralunb 3488 . . 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 3806 . . 3  |-  ( A  e.  V  ->  ( A. x  e.  { A } ph  <->  ps ) )
7 ralprg.2 . . . 4  |-  ( x  =  B  ->  ( ph 
<->  ch ) )
87ralsng 3806 . . 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 2666    u. cun 3278   {csn 3774   {cpr 3775
This theorem is referenced by:  raltpg  3819  ralpr  3821  iinxprg  4128  disjprg  4168  suppr  7429  injresinjlem  11154  gcdcllem2  12967  joinval2  14401  meetval2  14408  spwpr2  14615  iccntr  18805  limcun  19735  cusgra2v  21424  cusgra3v  21426  spthispth  21526  usgrcyclnl2  21581  4cycl4v4e  21606  4cycl4dv4e  21608  sumpr  24171  prsiga  24467  f12dfv  27961  f13dfv  27962  usgra2pthlem1  28040  usgra2pth  28041  frgra2v  28103  frgra3v  28106  3vfriswmgra  28109
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 2385
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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-v 2918  df-sbc 3122  df-un 3285  df-sn 3780  df-pr 3781
  Copyright terms: Public domain W3C validator