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

Theorem ralprg 4078
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:   ,   ,   ,   ,

Proof of Theorem ralprg
StepHypRef Expression
1 df-pr 4032 . . . 4
21raleqi 3058 . . 3
3 ralunb 3684 . . 3
42, 3bitri 249 . 2
5 ralprg.1 . . . 4
65ralsng 4064 . . 3
7 ralprg.2 . . . 4
87ralsng 4064 . . 3
96, 8bi2anan9 873 . 2
104, 9syl5bb 257 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  A.wral 2807  u.cun 3473  {csn 4029  {cpr 4031
This theorem is referenced by:  raltpg  4080  ralpr  4082  iinxprg  4408  disjprg  4448  f12dfv  6179  f13dfv  6180  suppr  7950  injresinjlem  11925  gcdcllem2  14150  joinval2lem  15638  meetval2lem  15652  sgrp2rid2  16044  sgrp2nmndlem4  16046  sgrp2nmndlem5  16047  iccntr  21326  limcun  22299  cusgra2v  24462  cusgra3v  24464  spthispth  24575  4cycl4v4e  24666  4cycl4dv4e  24668  frgra3v  25002  3vfriswmgra  25005  sumpr  27769  prsiga  28131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-v 3111  df-sbc 3328  df-un 3480  df-sn 4030  df-pr 4032
  Copyright terms: Public domain W3C validator