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
ralprg.2
Assertion
Ref Expression
ralprg
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem ralprg
StepHypRef Expression
1 df-pr 3850 . . . 4
21raleqi 2915 . . 3
3 ralunb 3517 . . 3
42, 3bitri 242 . 2
5 ralprg.1 . . . 4
65ralsng 3875 . . 3
7 ralprg.2 . . . 4
87ralsng 3875 . . 3
96, 8bi2anan9 845 . 2
104, 9syl5bb 250 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360   wceq 1654   wcel 1728  wral 2712   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