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

Theorem ralrimivva 2635
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 2634 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 1684   A.wral 2543
This theorem is referenced by:  disjxiun  4020  swopo  4324  issod  4344  fcof1  5797  fliftfund  5812  soisores  5824  soisoi  5825  isocnv  5827  f1oiso  5848  caovclg  6012  caovcomg  6015  off  6093  caofrss  6110  caonncan  6115  fmpt2co  6202  poxp  6227  smo11  6381  smoiso2  6386  omsmo  6652  qsdisj2  6737  eroprf  6756  dom2lem  6901  omxpenlem  6963  xpf1o  7023  unxpdomlem3  7069  fofinf1o  7137  dffi3  7184  supmo  7203  inf3lem6  7334  cantnf  7395  rankxplim  7549  fseqenlem1  7651  fodomacn  7683  iunfictbso  7741  cofsmo  7895  infpssrlem5  7933  enfin2i  7947  fin23lem23  7952  fin23lem27  7954  fin23lem28  7966  compssiso  8000  ltordlem  9298  cju  9742  axdc4uzlem  11044  seqcaopr2  11082  seqhomo  11093  climcn2  12066  addcn2  12067  mulcn2  12069  o1of2  12086  isercolllem1  12138  fsum2dlem  12233  fsumcom2  12237  isprm6  12788  crt  12846  eulerthlem2  12850  vdwlem12  13039  imasaddfnlem  13430  imasvscafn  13439  mreexexd  13550  iscatd  13575  proplem  13592  oppccomfpropd  13630  sectmon  13680  ssctr  13702  ssceq  13703  issubc3  13723  fullsubc  13724  fullresc  13725  isfuncd  13739  idfucl  13755  cofucl  13762  funcres2b  13771  fulloppc  13796  fthoppc  13797  idffth  13807  cofull  13808  cofth  13809  ressffth  13812  setcmon  13919  setcepi  13920  resssetc  13924  resscatc  13937  catciso  13939  evlfcl  13996  uncfcurf  14013  hofcl  14033  yonedalem3  14054  yonedainv  14055  yonffthlem  14056  yoniso  14059  isdrs2  14073  isposd  14089  pospropd  14238  poslubmo  14250  mndplusf  14383  mndfo  14397  mndpropd  14398  issubmnd  14401  mhmpropd  14421  0mhm  14435  resmhm  14436  resmhm2  14437  resmhm2b  14438  mhmco  14439  submacs  14442  prdspjmhm  14443  pwsdiagmhm  14445  pwsco1mhm  14446  pwsco2mhm  14447  gsumwspan  14468  frmdsssubm  14483  frmdup1  14486  grpsubf  14545  issubg4  14638  isnsg3  14651  nsgacs  14653  0nsg  14662  nsgid  14663  isghmd  14692  ghmmhm  14693  idghm  14698  ghmnsgima  14706  ghmnsgpreima  14707  ghmf1  14711  ghmf1o  14712  gaid  14753  subgga  14754  gass  14755  gasubg  14756  lactghmga  14784  cntzsubm  14811  cntrsubgnsg  14816  odf1  14875  sylow1lem2  14910  sylow2blem2  14932  sylow3lem1  14938  lsmssv  14954  lsmidm  14973  pj1eu  15005  efglem  15025  efgtf  15031  efgred  15057  efgredeu  15061  frgpmhm  15074  frgpuptf  15079  frgpuplem  15081  mulgmhm  15127  invghm  15130  ablnsg  15139  gsum2d2lem  15224  gsum2d2  15225  gsumcom2  15226  dprd2d2  15279  ablfaclem2  15321  isrhm2d  15506  issubrg2  15565  subrgint  15567  islmodd  15633  lmodscaf  15649  lmodprop2d  15687  islssd  15693  islss4  15719  lssacs  15724  lsspropd  15774  islmhmd  15796  lmhmima  15804  lmhmpreima  15805  reslmhm  15809  lspextmo  15813  lsmcl  15836  pj1lmhm  15853  islbs2  15907  issubrngd2  15943  opprdomn  16042  abvn0b  16043  issubassa2  16084  mvrf1  16170  mplsubglem  16179  mplsubrg  16184  mplind  16243  evlslem2  16249  ply1sclf1  16364  prmirredlem  16446  expmhm  16449  expghm  16450  mulgghm2  16459  domnchr  16486  znf1o  16505  zntoslem  16510  znfld  16514  cygznlem3  16523  phlipf  16556  tgclb  16708  mretopd  16829  toponmre  16830  iscldtop  16832  ordtbaslem  16918  ordtbas2  16921  cnt0  17074  haust1  17080  cnhaus  17082  isreg2  17105  dishaus  17110  ordthaus  17112  dfcon2  17145  iuncon  17154  clscon  17156  2ndcomap  17184  dis2ndc  17186  llynlly  17203  restnlly  17208  restlly  17209  islly2  17210  llyidm  17214  nllyidm  17215  hausllycmp  17220  kgentopon  17233  txbas  17262  ptbasin2  17273  ptbasfi  17276  txcnp  17314  txcnmpt  17318  pthaus  17332  tx1stc  17344  xkococnlem  17353  xkococn  17354  cnmpt21  17365  qtoptop2  17390  qtopeu  17407  kqt0lem  17427  isr0  17428  regr1lem2  17431  kqreglem1  17432  kqreglem2  17433  kqnrmlem1  17434  kqnrmlem2  17435  nrmr0reg  17440  reghmph  17484  nrmhmph  17485  txswaphmeo  17496  qtophmeo  17508  fbun  17535  trfbas2  17538  isfil2  17551  infil  17558  trfil2  17582  filssufilg  17606  hausflim  17676  fclsnei  17714  fclsfnflim  17722  flimfnfcls  17723  ptcmplem1  17746  clssubg  17791  tgpconcomp  17795  divstgplem  17803  tsmsfbas  17810  isxmetd  17891  isxmet2d  17892  xmettpos  17913  prdsdsf  17931  prdsmet  17934  ressprdsds  17935  imasdsf1olem  17937  imasf1oxmet  17939  imasf1omet  17940  blfval  17947  xmetresbl  17983  metss2  18058  comet  18059  stdbdmet  18062  stdbdmopn  18064  methaus  18066  met2ndci  18068  nrmmetd  18097  subgngp  18151  ngptgp  18152  sranlm  18195  nlmvscnlem1  18197  nlmvscn  18198  nrginvrcn  18202  lssnlm  18211  nghmcn  18254  qtopbaslem  18267  reconn  18333  xmetdcn2  18342  metdscn  18360  metnrm  18366  elcncf1di  18399  cncffvrn  18402  mulc1cncf  18409  cncfco  18411  reparphti  18495  tchcph  18667  ipcnlem1  18672  ipcn  18673  iscfil3  18699  bcthlem5  18750  minveclem3  18793  minveclem7  18799  ovolicc2lem4  18879  dyadmbl  18955  volcn  18961  itg1addlem1  19047  itg1addlem2  19052  itg1addlem4  19054  mbfi1fseqlem1  19070  mbfi1fseqlem3  19072  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  dvmptfsum  19322  c1liplem1  19343  dvgt0lem2  19350  ftc1a  19384  evlseu  19400  ply1domn  19509  ply1divmo  19521  fta1b  19555  ig1peu  19557  coeeu  19607  plydivalg  19679  aaliou2b  19721  ulmss  19774  ulmcn  19776  efif1olem4  19907  logccv  20010  cvxcl  20279  basellem4  20321  fsumdvdscom  20425  musum  20431  dvdsmulf1o  20434  fsumdvdsmul  20435  dchrelbasd  20478  dchrmulcl  20488  dchrinv  20500  lgsqrlem2  20581  lgsdchr  20587  lgseisenlem2  20589  lgsquadlem1  20593  lgsquadlem2  20594  dchrisumlema  20637  dchrisumlem2  20639  chpdifbndlem2  20703  pntpbnd  20737  pntibndlem3  20741  isgrp2d  20902  grpoinvf  20907  subgoablo  20978  ghgrplem2  21034  ghablo  21036  nvmf  21204  vacn  21267  nmcvcn  21268  smcnlem  21270  sspg  21304  ssps  21306  sspmlem  21308  0lno  21368  blocni  21383  sspph  21433  ipblnfi  21434  minvecolem7  21462  unopf1o  22496  cnvunop  22498  unoplin  22500  counop  22501  hmopadj2  22521  hmoplin  22522  bralnfn  22528  lnopeq0i  22587  hmops  22600  hmopm  22601  hmopco  22603  lnconi  22613  cnlnadjlem2  22648  adjmul  22672  adjadd  22673  cdjreui  23012  off2  23208  xrofsup  23255  ofcf  23464  erdszelem4  23725  erdszelem9  23730  erdsze2lem2  23735  cnpcon  23761  pconcon  23762  txpcon  23763  ptpcon  23764  cvxpcon  23773  cvxscon  23774  iccllyscon  23781  cvmseu  23807  cvmliftmo  23815  cvmlift2lem5  23838  cvmlift2lem9  23842  brbtwn2  24533  axlowdimlem15  24584  axcontlem2  24593  axcontlem10  24601  segconeu  24634  onsuct0  24880  toplat  25290  trooo  25394  rltrooo  25415  muldisc  25481  trnij  25615  sigadd  25649  fnmulcv  25684  icccon2  25700  icccon3  25701  icccon4  25702  idmon  25817  prismorcsetlemb  25913  setiscat  25979  fnessref  26293  neibastop1  26308  filnetlem3  26329  r19.21aivvaOLD  26338  sdclem1  26453  isbnd3  26508  prdsbnd  26517  ismtycnv  26526  ismtyhmeolem  26528  ismtyres  26532  bfplem1  26546  bfplem2  26547  bfp  26548  rrnmet  26553  ismrer1  26562  iccbnd  26564  grpokerinj  26575  isdrngo2  26589  rngogrphom  26602  rngohomco  26605  rngoisocnv  26612  iscringd  26624  erprt  26741  nacsfix  26787  rmxypairf1o  26996  wepwsolem  27138  dnnumch3  27144  fnwe2  27150  dsmmlss  27210  uvcf1  27241  frlmlbs  27249  lindff1  27290  lindfrn  27291  f1lindf  27292  mpaaeu  27355  issubmd  27383  mamucl  27456  mamudiagcl  27457  mamulid  27458  mamurid  27459  mamuass  27460  mamudi  27461  mamudir  27462  mamuvs1  27463  mamuvs2  27464  idomsubgmo  27514  mon1psubm  27525  deg1mhm  27526  dmmpt2g  27981  lfl0f  29259  lkrlss  29285  lshpsmreu  29299  linepsubN  29941  pmapsub  29957  lautcnv  30279  lautco  30286  idltrn  30339  cdleme50f1  30732  cdleme50laut  30736  istendod  30951  dihf11  31457  dih1dimatlem  31519  lcfl7N  31691  lcfrlem9  31740  mapd1o  31838  hdmapf1oN  32058  hgmapf1oN  32096
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532  df-ral 2548
  Copyright terms: Public domain W3C validator