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

Theorem ralprg 4032
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 3987 . . . 4  |-  { A ,  B }  =  ( { A }  u.  { B } )
21raleqi 3025 . . 3  |-  ( A. x  e.  { A ,  B } ph  <->  A. x  e.  ( { A }  u.  { B } )
ph )
3 ralunb 3644 . . 3  |-  ( A. x  e.  ( { A }  u.  { B } ) ph  <->  ( A. x  e.  { A } ph  /\  A. x  e.  { B } ph ) )
42, 3bitri 249 . 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 4019 . . 3  |-  ( A  e.  V  ->  ( A. x  e.  { A } ph  <->  ps ) )
7 ralprg.2 . . . 4  |-  ( x  =  B  ->  ( ph 
<->  ch ) )
87ralsng 4019 . . 3  |-  ( B  e.  W  ->  ( A. x  e.  { B } ph  <->  ch ) )
96, 8bi2anan9 868 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( ( A. x  e.  { A } ph  /\ 
A. x  e.  { B } ph )  <->  ( ps  /\ 
ch ) ) )
104, 9syl5bb 257 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( 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 2798    u. cun 3433   {csn 3984   {cpr 3986
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 2803  df-v 3078  df-sbc 3293  df-un 3440  df-sn 3985  df-pr 3987
This theorem is referenced by:  raltpg  4034  ralpr  4036  iinxprg  4355  disjprg  4395  suppr  7828  injresinjlem  11754  gcdcllem2  13813  joinval2lem  15296  meetval2lem  15310  iccntr  20529  limcun  21502  cusgra2v  23521  cusgra3v  23523  spthispth  23623  usgrcyclnl2  23678  4cycl4v4e  23703  4cycl4dv4e  23705  sumpr  26386  prsiga  26718  f12dfv  30293  f13dfv  30294  wwlktovf1  30399  usgra2pthlem1  30447  usgra2pth  30448  frgra3v  30741  3vfriswmgra  30744
  Copyright terms: Public domain W3C validator