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

Theorem ralprg 3886
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 3850 . . . 4  |-  { A ,  B }  =  ( { A }  u.  { B } )
21raleqi 2915 . . 3  |-  ( A. x  e.  { A ,  B } ph  <->  A. x  e.  ( { A }  u.  { B } )
ph )
3 ralunb 3517 . . 3  |-  ( A. x  e.  ( { A }  u.  { B } ) ph  <->  ( A. x  e.  { A } ph  /\  A. x  e.  { B } ph ) )
42, 3bitri 242 . 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 3875 . . 3  |-  ( A  e.  V  ->  ( A. x  e.  { A } ph  <->  ps ) )
7 ralprg.2 . . . 4  |-  ( x  =  B  ->  ( ph 
<->  ch ) )
87ralsng 3875 . . 3  |-  ( B  e.  W  ->  ( A. x  e.  { B } ph  <->  ch ) )
96, 8bi2anan9 845 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( ( A. x  e.  { A } ph  /\ 
A. x  e.  { B } ph )  <->  ( ps  /\ 
ch ) ) )
104, 9syl5bb 250 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 178    /\ wa 360    = wceq 1654    e. wcel 1728   A.wral 2712    u. cun 3307   {csn 3843   {cpr 3844
This theorem is referenced by:  raltpg  3888  ralpr  3890  iinxprg  4199  disjprg  4239  suppr  7509  injresinjlem  11237  gcdcllem2  13050  joinval2  14484  meetval2  14491  spwpr2  14698  iccntr  18890  limcun  19820  cusgra2v  21509  cusgra3v  21511  spthispth  21611  usgrcyclnl2  21666  4cycl4v4e  21691  4cycl4dv4e  21693  sumpr  24253  prsiga  24549  f12dfv  28196  f13dfv  28197  usgra2pthlem1  28446  usgra2pth  28447  frgra2v  28561  frgra3v  28564  3vfriswmgra  28567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ral 2717  df-v 2967  df-sbc 3171  df-un 3314  df-sn 3849  df-pr 3850
  Copyright terms: Public domain W3C validator