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

Theorem ralrimivva 2648
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 423 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ps ) )
32ralrimivv 2647 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1696   A.wral 2556
This theorem is referenced by:  disjxiun  4036  swopo  4340  issod  4360  fcof1  5813  fliftfund  5828  soisores  5840  soisoi  5841  isocnv  5843  f1oiso  5864  caovclg  6028  caovcomg  6031  off  6109  caofrss  6126  caonncan  6131  fmpt2co  6218  poxp  6243  smo11  6397  smoiso2  6402  omsmo  6668  qsdisj2  6753  eroprf  6772  dom2lem  6917  omxpenlem  6979  xpf1o  7039  unxpdomlem3  7085  fofinf1o  7153  dffi3  7200  supmo  7219  inf3lem6  7350  cantnf  7411  rankxplim  7565  fseqenlem1  7667  fodomacn  7699  iunfictbso  7757  cofsmo  7911  infpssrlem5  7949  enfin2i  7963  fin23lem23  7968  fin23lem27  7970  fin23lem28  7982  compssiso  8016  ltordlem  9314  cju  9758  axdc4uzlem  11060  seqcaopr2  11098  seqhomo  11109  climcn2  12082  addcn2  12083  mulcn2  12085  o1of2  12102  isercolllem1  12154  fsum2dlem  12249  fsumcom2  12253  isprm6  12804  crt  12862  eulerthlem2  12866  vdwlem12  13055  imasaddfnlem  13446  imasvscafn  13455  mreexexd  13566  iscatd  13591  proplem  13608  oppccomfpropd  13646  sectmon  13696  ssctr  13718  ssceq  13719  issubc3  13739  fullsubc  13740  fullresc  13741  isfuncd  13755  idfucl  13771  cofucl  13778  funcres2b  13787  fulloppc  13812  fthoppc  13813  idffth  13823  cofull  13824  cofth  13825  ressffth  13828  setcmon  13935  setcepi  13936  resssetc  13940  resscatc  13953  catciso  13955  evlfcl  14012  uncfcurf  14029  hofcl  14049  yonedalem3  14070  yonedainv  14071  yonffthlem  14072  yoniso  14075  isdrs2  14089  isposd  14105  pospropd  14254  poslubmo  14266  mndplusf  14399  mndfo  14413  mndpropd  14414  issubmnd  14417  mhmpropd  14437  0mhm  14451  resmhm  14452  resmhm2  14453  resmhm2b  14454  mhmco  14455  submacs  14458  prdspjmhm  14459  pwsdiagmhm  14461  pwsco1mhm  14462  pwsco2mhm  14463  gsumwspan  14484  frmdsssubm  14499  frmdup1  14502  grpsubf  14561  issubg4  14654  isnsg3  14667  nsgacs  14669  0nsg  14678  nsgid  14679  isghmd  14708  ghmmhm  14709  idghm  14714  ghmnsgima  14722  ghmnsgpreima  14723  ghmf1  14727  ghmf1o  14728  gaid  14769  subgga  14770  gass  14771  gasubg  14772  lactghmga  14800  cntzsubm  14827  cntrsubgnsg  14832  odf1  14891  sylow1lem2  14926  sylow2blem2  14948  sylow3lem1  14954  lsmssv  14970  lsmidm  14989  pj1eu  15021  efglem  15041  efgtf  15047  efgred  15073  efgredeu  15077  frgpmhm  15090  frgpuptf  15095  frgpuplem  15097  mulgmhm  15143  invghm  15146  ablnsg  15155  gsum2d2lem  15240  gsum2d2  15241  gsumcom2  15242  dprd2d2  15295  ablfaclem2  15337  isrhm2d  15522  issubrg2  15581  subrgint  15583  islmodd  15649  lmodscaf  15665  lmodprop2d  15703  islssd  15709  islss4  15735  lssacs  15740  lsspropd  15790  islmhmd  15812  lmhmima  15820  lmhmpreima  15821  reslmhm  15825  lspextmo  15829  lsmcl  15852  pj1lmhm  15869  islbs2  15923  issubrngd2  15959  opprdomn  16058  abvn0b  16059  issubassa2  16100  mvrf1  16186  mplsubglem  16195  mplsubrg  16200  mplind  16259  evlslem2  16265  ply1sclf1  16380  prmirredlem  16462  expmhm  16465  expghm  16466  mulgghm2  16475  domnchr  16502  znf1o  16521  zntoslem  16526  znfld  16530  cygznlem3  16539  phlipf  16572  tgclb  16724  mretopd  16845  toponmre  16846  iscldtop  16848  ordtbaslem  16934  ordtbas2  16937  cnt0  17090  haust1  17096  cnhaus  17098  isreg2  17121  dishaus  17126  ordthaus  17128  dfcon2  17161  iuncon  17170  clscon  17172  2ndcomap  17200  dis2ndc  17202  llynlly  17219  restnlly  17224  restlly  17225  islly2  17226  llyidm  17230  nllyidm  17231  hausllycmp  17236  kgentopon  17249  txbas  17278  ptbasin2  17289  ptbasfi  17292  txcnp  17330  txcnmpt  17334  pthaus  17348  tx1stc  17360  xkococnlem  17369  xkococn  17370  cnmpt21  17381  qtoptop2  17406  qtopeu  17423  kqt0lem  17443  isr0  17444  regr1lem2  17447  kqreglem1  17448  kqreglem2  17449  kqnrmlem1  17450  kqnrmlem2  17451  nrmr0reg  17456  reghmph  17500  nrmhmph  17501  txswaphmeo  17512  qtophmeo  17524  fbun  17551  trfbas2  17554  isfil2  17567  infil  17574  trfil2  17598  filssufilg  17622  hausflim  17692  fclsnei  17730  fclsfnflim  17738  flimfnfcls  17739  ptcmplem1  17762  clssubg  17807  tgpconcomp  17811  divstgplem  17819  tsmsfbas  17826  isxmetd  17907  isxmet2d  17908  xmettpos  17929  prdsdsf  17947  prdsmet  17950  ressprdsds  17951  imasdsf1olem  17953  imasf1oxmet  17955  imasf1omet  17956  blfval  17963  xmetresbl  17999  metss2  18074  comet  18075  stdbdmet  18078  stdbdmopn  18080  methaus  18082  met2ndci  18084  nrmmetd  18113  subgngp  18167  ngptgp  18168  sranlm  18211  nlmvscnlem1  18213  nlmvscn  18214  nrginvrcn  18218  lssnlm  18227  nghmcn  18270  qtopbaslem  18283  reconn  18349  xmetdcn2  18358  metdscn  18376  metnrm  18382  elcncf1di  18415  cncffvrn  18418  mulc1cncf  18425  cncfco  18427  reparphti  18511  tchcph  18683  ipcnlem1  18688  ipcn  18689  iscfil3  18715  bcthlem5  18766  minveclem3  18809  minveclem7  18815  ovolicc2lem4  18895  dyadmbl  18971  volcn  18977  itg1addlem1  19063  itg1addlem2  19068  itg1addlem4  19070  mbfi1fseqlem1  19086  mbfi1fseqlem3  19088  mbfi1fseqlem4  19089  mbfi1fseqlem5  19090  dvmptfsum  19338  c1liplem1  19359  dvgt0lem2  19366  ftc1a  19400  evlseu  19416  ply1domn  19525  ply1divmo  19537  fta1b  19571  ig1peu  19573  coeeu  19623  plydivalg  19695  aaliou2b  19737  ulmss  19790  ulmcn  19792  efif1olem4  19923  logccv  20026  cvxcl  20295  basellem4  20337  fsumdvdscom  20441  musum  20447  dvdsmulf1o  20450  fsumdvdsmul  20451  dchrelbasd  20494  dchrmulcl  20504  dchrinv  20516  lgsqrlem2  20597  lgsdchr  20603  lgseisenlem2  20605  lgsquadlem1  20609  lgsquadlem2  20610  dchrisumlema  20653  dchrisumlem2  20655  chpdifbndlem2  20719  pntpbnd  20753  pntibndlem3  20757  isgrp2d  20918  grpoinvf  20923  subgoablo  20994  ghgrplem2  21050  ghablo  21052  nvmf  21220  vacn  21283  nmcvcn  21284  smcnlem  21286  sspg  21320  ssps  21322  sspmlem  21324  0lno  21384  blocni  21399  sspph  21449  ipblnfi  21450  minvecolem7  21478  unopf1o  22512  cnvunop  22514  unoplin  22516  counop  22517  hmopadj2  22537  hmoplin  22538  bralnfn  22544  lnopeq0i  22603  hmops  22616  hmopm  22617  hmopco  22619  lnconi  22629  cnlnadjlem2  22664  adjmul  22688  adjadd  22689  cdjreui  23028  off2  23223  xrofsup  23270  ofcf  23479  erdszelem4  23740  erdszelem9  23745  erdsze2lem2  23750  cnpcon  23776  pconcon  23777  txpcon  23778  ptpcon  23779  cvxpcon  23788  cvxscon  23789  iccllyscon  23796  cvmseu  23822  cvmliftmo  23830  cvmlift2lem5  23853  cvmlift2lem9  23857  brbtwn2  24605  axlowdimlem15  24656  axcontlem2  24665  axcontlem10  24673  segconeu  24706  onsuct0  24952  toplat  25393  trooo  25497  rltrooo  25518  muldisc  25584  trnij  25718  sigadd  25752  fnmulcv  25787  icccon2  25803  icccon3  25804  icccon4  25805  idmon  25920  prismorcsetlemb  26016  setiscat  26082  fnessref  26396  neibastop1  26411  filnetlem3  26432  r19.21aivvaOLD  26441  sdclem1  26556  isbnd3  26611  prdsbnd  26620  ismtycnv  26629  ismtyhmeolem  26631  ismtyres  26635  bfplem1  26649  bfplem2  26650  bfp  26651  rrnmet  26656  ismrer1  26665  iccbnd  26667  grpokerinj  26678  isdrngo2  26692  rngogrphom  26705  rngohomco  26708  rngoisocnv  26715  iscringd  26727  erprt  26844  nacsfix  26890  rmxypairf1o  27099  wepwsolem  27241  dnnumch3  27247  fnwe2  27253  dsmmlss  27313  uvcf1  27344  frlmlbs  27352  lindff1  27393  lindfrn  27394  f1lindf  27395  mpaaeu  27458  issubmd  27486  mamucl  27559  mamudiagcl  27560  mamulid  27561  mamurid  27562  mamuass  27563  mamudi  27564  mamudir  27565  mamuvs1  27566  mamuvs2  27567  idomsubgmo  27617  mon1psubm  27628  deg1mhm  27629  dmmpt2g  28086  lfl0f  29881  lkrlss  29907  lshpsmreu  29921  linepsubN  30563  pmapsub  30579  lautcnv  30901  lautco  30908  idltrn  30961  cdleme50f1  31354  cdleme50laut  31358  istendod  31573  dihf11  32079  dih1dimatlem  32141  lcfl7N  32313  lcfrlem9  32362  mapd1o  32460  hdmapf1oN  32680  hgmapf1oN  32718
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1535  df-ral 2561
  Copyright terms: Public domain W3C validator