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

Theorem ralrimivva 2885
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by Jeff Madsen, 19-Jun-2011.)
Hypothesis
Ref Expression
ralrimivva.1  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  ->  ps )
Assertion
Ref Expression
ralrimivva  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Distinct variable groups:    ph, x, y   
y, A
Allowed substitution hints:    ps( x, y)    A( x)    B( x, y)

Proof of Theorem ralrimivva
StepHypRef Expression
1 ralrimivva.1 . . 3  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  ->  ps )
21ex 434 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ps ) )
32ralrimivv 2884 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2819
This theorem is referenced by:  disjxiun  4444  otsndisj  4752  otiunsndisj  4753  swopo  4810  issod  4830  fcof1  6176  fliftfund  6197  soisores  6209  soisoi  6210  isocnv  6212  f1oiso  6233  caovclg  6449  caovcomg  6452  off  6536  caofrss  6555  caonncan  6560  dmmpt2g  6853  fnmpt2ovd  6858  fmpt2co  6863  poxp  6892  fvmpt2curryd  6997  smo11  7032  smoiso2  7037  omsmo  7300  qsdisj2  7386  eroprf  7406  dom2lem  7552  omxpenlem  7615  xpf1o  7676  unxpdomlem3  7723  fofinf1o  7797  dffi3  7887  supmo  7908  inf3lem6  8046  cantnf  8108  cantnfOLD  8130  rankxplim  8293  fseqenlem1  8401  fodomacn  8433  iunfictbso  8491  cofsmo  8645  infpssrlem5  8683  enfin2i  8697  fin23lem23  8702  fin23lem27  8704  fin23lem28  8716  compssiso  8750  ltordlem  10074  cju  10528  axdc4uzlem  12055  seqcaopr2  12106  seqhomo  12117  wrd2ind  12660  climcn2  13371  addcn2  13372  mulcn2  13374  o1of2  13391  isercolllem1  13443  fsum2dlem  13541  fsumcom2  13545  isprm6  14102  crt  14160  eulerthlem2  14164  vdwlem12  14362  cshwsdisj  14434  imasaddfnlem  14776  imasvscafn  14785  mreexexd  14896  iscatd  14921  proplem  14938  oppccomfpropd  14976  sectmon  15026  ssctr  15048  ssceq  15049  issubc3  15069  fullsubc  15070  fullresc  15071  isfuncd  15085  idfucl  15101  cofucl  15108  funcres2b  15117  fulloppc  15142  fthoppc  15143  idffth  15153  cofull  15154  cofth  15155  ressffth  15158  setcmon  15265  setcepi  15266  resssetc  15270  resscatc  15283  catciso  15285  evlfcl  15342  uncfcurf  15359  hofcl  15379  yonedalem3  15400  yonedainv  15401  yonffthlem  15402  yoniso  15405  isdrs2  15419  isposd  15435  pospropd  15614  poslubmo  15626  posglbmo  15627  mndplusf  15741  mndfo  15755  mndpropd  15756  issubmnd  15759  mhmpropd  15780  mhmf1o  15783  issubmd  15787  0mhm  15796  resmhm  15797  resmhm2  15798  resmhm2b  15799  mhmco  15800  submacs  15803  prdspjmhm  15805  pwsdiagmhm  15807  pwsco1mhm  15808  pwsco2mhm  15809  gsumwspan  15834  frmdsssubm  15849  frmdup1  15852  grpsubf  15915  issubg4  16012  grpissubg  16013  isnsg3  16027  nsgacs  16029  0nsg  16038  nsgid  16039  isghmd  16068  ghmmhm  16069  idghm  16074  ghmnsgima  16082  ghmnsgpreima  16083  ghmf1  16087  ghmf1o  16088  gaid  16129  subgga  16130  gass  16131  gasubg  16132  cntzsubm  16165  cntrsubgnsg  16170  lactghmga  16221  odf1  16377  sylow1lem2  16412  sylow2blem2  16434  sylow3lem1  16440  lsmssv  16456  lsmidm  16475  pj1eu  16507  efglem  16527  efgtf  16533  efgred  16559  efgredeu  16563  frgpmhm  16576  frgpuptf  16581  frgpuplem  16583  mulgmhm  16629  invghm  16632  ablnsg  16643  gsum2d2lem  16789  gsum2d2  16790  gsumcom2  16791  dprd2d2  16880  ablfaclem2  16924  srglmhm  16971  srgrmhm  16972  isrhm2d  17158  kerf1hrm  17172  issubrg2  17229  subrgint  17231  islmodd  17298  lmodscaf  17314  lmodprop2d  17352  islssd  17362  islss4  17388  lssacs  17393  lsspropd  17443  islmhmd  17465  lmhmima  17473  lmhmpreima  17474  reslmhm  17478  lspextmo  17482  lsmcl  17509  pj1lmhm  17526  islbs2  17580  issubrngd2  17615  opprdomn  17718  abvn0b  17719  issubassa2  17762  mvrf1  17849  mplsubglem  17861  mplsubglemOLD  17863  mplsubrg  17870  mplcoe5lem  17898  mplcoe2  17900  mplind  17935  evlslem2  17948  evlseu  17953  ply1sclf1  18098  expmhm  18250  nn0srg  18251  prmirredlem  18287  prmirredlemOLD  18290  expghm  18293  expghmOLD  18294  mulgghm2  18295  mulgghm2OLD  18298  domnchr  18333  znf1o  18354  zntoslem  18359  znfld  18363  cygznlem3  18372  phlipf  18451  dsmmlss  18539  uvcf1  18587  frlmlbs  18595  lindff1  18619  lindfrn  18620  f1lindf  18621  mamucl  18667  mamuass  18668  mamudi  18669  mamudir  18670  mamuvs1  18671  mamuvs2  18672  matbas2d  18689  mamumat1cl  18705  mamulid  18707  mamurid  18708  mat1mhm  18750  dmatid  18761  dmatsubcl  18764  dmatsgrp  18765  dmatmulcl  18766  dmatsrng  18767  dmatcrng  18768  scmatscmiddistr  18774  scmatscm  18779  scmatsgrp  18785  scmatsrng  18786  scmatcrng  18787  scmatsgrp1  18788  scmatsrng1  18789  scmatf1  18797  scmatmhm  18800  mavmul0g  18819  mdet1  18867  mdetunilem9  18886  mdetuni0  18887  mdetmul  18889  madutpos  18908  smadiadetlem4  18935  1elcpmat  18980  cpmatacl  18981  cpmatmcl  18984  mat2pmatf1  18994  mat2pmatmul  18996  mat2pmat1  18997  mat2pmatlin  19000  m2cpm  19006  m2cpminvid  19018  m2cpminvid2  19020  decpmatmul  19037  pmatcollpw1  19041  monmatcollpw  19044  pmatcollpw  19046  pmatcollpw3lem  19048  pmatcollpwscmatlem2  19055  pm2mpf1  19064  mp2pm2mplem4  19074  pm2mpmhmlem2  19084  chp0mat  19111  chpidmat  19112  tgclb  19235  mretopd  19356  toponmre  19357  iscldtop  19359  ordtbaslem  19452  ordtbas2  19455  cnt0  19610  haust1  19616  cnhaus  19618  isreg2  19641  dishaus  19646  ordthaus  19648  dfcon2  19683  iuncon  19692  clscon  19694  2ndcomap  19722  dis2ndc  19724  llynlly  19741  restnlly  19746  restlly  19747  islly2  19748  llyidm  19752  nllyidm  19753  hausllycmp  19758  kgentopon  19771  txbas  19800  ptbasin2  19811  ptbasfi  19814  txcnp  19853  txcnmpt  19857  pthaus  19871  tx1stc  19883  xkococnlem  19892  xkococn  19893  cnmpt21  19904  qtoptop2  19932  qtopeu  19949  kqt0lem  19969  isr0  19970  regr1lem2  19973  kqreglem1  19974  kqreglem2  19975  kqnrmlem1  19976  kqnrmlem2  19977  nrmr0reg  19982  reghmph  20026  nrmhmph  20027  txswaphmeo  20038  qtophmeo  20050  fbun  20073  trfbas2  20076  isfil2  20089  infil  20096  trfil2  20120  filssufilg  20144  hausflim  20214  fclsnei  20252  fclsfnflim  20260  flimfnfcls  20261  ptcmplem1  20284  clssubg  20339  tgpconcomp  20343  divstgplem  20351  tsmsfbas  20358  utoptop  20469  iducn  20518  cstucnd  20519  isxmetd  20561  isxmet2d  20562  xmettpos  20584  prdsdsf  20602  prdsmet  20605  ressprdsds  20606  imasdsf1olem  20608  imasf1oxmet  20610  imasf1omet  20611  blfvalps  20618  xmetresbl  20672  metss2  20747  comet  20748  stdbdmet  20751  stdbdmopn  20753  methaus  20755  met2ndci  20757  metustfbasOLD  20800  metustfbas  20801  nrmmetd  20827  subgngp  20881  ngptgp  20882  sranlm  20925  nlmvscnlem1  20927  nlmvscn  20928  nrginvrcn  20932  lssnlm  20941  nghmcn  20984  qtopbaslem  20997  reconn  21065  xmetdcn2  21074  metdscn  21092  metnrm  21098  elcncf1di  21131  cncffvrn  21134  mulc1cncf  21141  cncfco  21143  reparphti  21229  tchcph  21412  ipcnlem1  21417  ipcn  21418  iscfil3  21444  bcthlem5  21499  rrxmet  21567  minveclem3  21576  minveclem7  21582  ovolicc2lem4  21663  dyadmbl  21741  volcn  21747  itg1addlem1  21831  itg1addlem2  21836  itg1addlem4  21838  mbfi1fseqlem1  21854  mbfi1fseqlem3  21856  mbfi1fseqlem4  21857  mbfi1fseqlem5  21858  dvmptfsum  22108  c1liplem1  22129  dvgt0lem2  22136  ftc1a  22170  ply1domn  22256  ply1divmo  22268  fta1b  22302  ig1peu  22304  coeeu  22354  plydivalg  22426  aaliou2b  22468  ulmss  22523  ulmcn  22525  efif1olem4  22662  logccv  22769  cvxcl  23039  basellem4  23082  fsumdvdscom  23186  musum  23192  dvdsmulf1o  23195  fsumdvdsmul  23196  dchrelbasd  23239  dchrmulcl  23249  dchrinv  23261  lgsqrlem2  23342  lgsdchr  23348  lgseisenlem2  23350  lgsquadlem1  23354  lgsquadlem2  23355  dchrisumlema  23398  dchrisumlem2  23400  chpdifbndlem2  23464  pntpbnd  23498  pntibndlem3  23502  axtgcont  23591  ercgrg  23633  idmot  23649  motco  23652  cnvmot  23653  motcgrg  23656  legso  23709  tgisline  23718  tghilbert1_2  23729  mirreu3  23745  mirmot  23765  ragperp  23799  foot  23801  mideu  23811  midf  23816  lmimot  23837  f1otrgds  23845  f1otrg  23847  f1otrge  23848  xmstrkgc  23862  brbtwn2  23881  axlowdimlem15  23932  axcontlem2  23941  axcontlem10  23949  eengtrkg  23961  eengtrkge  23962  usgraedgreu  24061  usgraidx2v  24066  wlknwwlkninj  24384  wlkiswwlkinj  24391  wwlkextinj  24403  clwwlkf1  24469  2spotiundisj  24736  2spotmdisj  24742  numclwlk1lem2f1  24768  isgrp2d  24910  grpoinvf  24915  subgoablo  24986  ghgrplem2  25042  ghablo  25044  nvmf  25214  vacn  25277  nmcvcn  25278  smcnlem  25280  sspg  25314  ssps  25316  sspmlem  25318  0lno  25378  blocni  25393  sspph  25443  ipblnfi  25444  minvecolem7  25472  unopf1o  26508  cnvunop  26510  unoplin  26512  counop  26513  hmopadj2  26533  hmoplin  26534  bralnfn  26540  lnopeq0i  26599  hmops  26612  hmopm  26613  hmopco  26615  lnconi  26625  cnlnadjlem2  26660  adjmul  26684  adjadd  26685  cdjreui  27024  disjxpin  27117  off2  27151  f1od2  27216  xrofsup  27247  odutos  27310  abliso  27345  archiabllem1  27396  archiabllem2  27400  suborng  27465  xrge0slmod  27494  pstmxmet  27509  ofcf  27739  sibfof  27919  erdszelem4  28275  erdszelem9  28280  erdsze2lem2  28285  cnpcon  28312  pconcon  28313  txpcon  28314  ptpcon  28315  cvxpcon  28324  cvxscon  28325  iccllyscon  28332  cvmseu  28358  cvmliftmo  28366  cvmlift2lem5  28389  cvmlift2lem9  28393  fprodser  28655  fprod2dlem  28684  fprodcom2  28688  segconeu  29235  onsuct0  29480  fin2so  29614  heicant  29624  mblfinlem2  29627  ftc1anc  29673  fnessref  29763  neibastop1  29778  filnetlem3  29799  sdclem1  29837  isbnd3  29881  prdsbnd  29890  ismtycnv  29899  ismtyhmeolem  29901  ismtyres  29905  bfplem1  29919  bfplem2  29920  bfp  29921  rrnmet  29926  ismrer1  29935  iccbnd  29937  grpokerinj  29948  isdrngo2  29962  rngogrphom  29975  rngohomco  29978  rngoisocnv  29985  iscringd  29997  erprt  30216  nacsfix  30246  rmxypairf1o  30449  wepwsolem  30591  dnnumch3  30597  fnwe2  30603  mpaaeu  30704  idomsubgmo  30760  mon1psubm  30771  deg1mhm  30772  sumnnodd  31172  lptioo2  31173  lptioo1  31174  cncfshift  31212  cncfperiod  31217  fourierdlem42  31449  otiunsndisjX  31768  usgvincvadeu  31874  usgvincvadeuALT  31877  usgedgvadf1  31884  usgedgvadf1ALT  31887  mgmcllaw  31963  lindslinindsimp1  32131  lmod1  32174  lfl0f  33866  lkrlss  33892  lshpsmreu  33906  linepsubN  34548  pmapsub  34564  lautcnv  34886  lautco  34893  idltrn  34946  cdleme50f1  35339  cdleme50laut  35343  istendod  35558  dihf11  36064  dih1dimatlem  36126  lcfl7N  36298  lcfrlem9  36347  mapd1o  36445  hdmapf1oN  36665  hgmapf1oN  36703
  Copyright terms: Public domain W3C validator