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

Theorem ralrimivva 2800
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 425 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ps ) )
32ralrimivv 2799 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    e. wcel 1726   A.wral 2707
This theorem is referenced by:  disjxiun  4212  swopo  4516  issod  4536  fcof1  6023  fliftfund  6038  soisores  6050  soisoi  6051  isocnv  6053  f1oiso  6074  caovclg  6242  caovcomg  6245  off  6323  caofrss  6340  caonncan  6345  fmpt2co  6433  poxp  6461  smo11  6629  smoiso2  6634  omsmo  6900  qsdisj2  6985  eroprf  7005  dom2lem  7150  omxpenlem  7212  xpf1o  7272  unxpdomlem3  7318  fofinf1o  7390  dffi3  7439  supmo  7460  inf3lem6  7591  cantnf  7652  rankxplim  7808  fseqenlem1  7910  fodomacn  7942  iunfictbso  8000  cofsmo  8154  infpssrlem5  8192  enfin2i  8206  fin23lem23  8211  fin23lem27  8213  fin23lem28  8225  compssiso  8259  ltordlem  9557  cju  10001  axdc4uzlem  11326  seqcaopr2  11364  seqhomo  11375  climcn2  12391  addcn2  12392  mulcn2  12394  o1of2  12411  isercolllem1  12463  fsum2dlem  12559  fsumcom2  12563  isprm6  13114  crt  13172  eulerthlem2  13176  vdwlem12  13365  imasaddfnlem  13758  imasvscafn  13767  mreexexd  13878  iscatd  13903  proplem  13920  oppccomfpropd  13958  sectmon  14008  ssctr  14030  ssceq  14031  issubc3  14051  fullsubc  14052  fullresc  14053  isfuncd  14067  idfucl  14083  cofucl  14090  funcres2b  14099  fulloppc  14124  fthoppc  14125  idffth  14135  cofull  14136  cofth  14137  ressffth  14140  setcmon  14247  setcepi  14248  resssetc  14252  resscatc  14265  catciso  14267  evlfcl  14324  uncfcurf  14341  hofcl  14361  yonedalem3  14382  yonedainv  14383  yonffthlem  14384  yoniso  14387  isdrs2  14401  isposd  14417  pospropd  14566  poslubmo  14578  mndplusf  14711  mndfo  14725  mndpropd  14726  issubmnd  14729  mhmpropd  14749  0mhm  14763  resmhm  14764  resmhm2  14765  resmhm2b  14766  mhmco  14767  submacs  14770  prdspjmhm  14771  pwsdiagmhm  14773  pwsco1mhm  14774  pwsco2mhm  14775  gsumwspan  14796  frmdsssubm  14811  frmdup1  14814  grpsubf  14873  issubg4  14966  isnsg3  14979  nsgacs  14981  0nsg  14990  nsgid  14991  isghmd  15020  ghmmhm  15021  idghm  15026  ghmnsgima  15034  ghmnsgpreima  15035  ghmf1  15039  ghmf1o  15040  gaid  15081  subgga  15082  gass  15083  gasubg  15084  lactghmga  15112  cntzsubm  15139  cntrsubgnsg  15144  odf1  15203  sylow1lem2  15238  sylow2blem2  15260  sylow3lem1  15266  lsmssv  15282  lsmidm  15301  pj1eu  15333  efglem  15353  efgtf  15359  efgred  15385  efgredeu  15389  frgpmhm  15402  frgpuptf  15407  frgpuplem  15409  mulgmhm  15455  invghm  15458  ablnsg  15467  gsum2d2lem  15552  gsum2d2  15553  gsumcom2  15554  dprd2d2  15607  ablfaclem2  15649  isrhm2d  15834  issubrg2  15893  subrgint  15895  islmodd  15961  lmodscaf  15977  lmodprop2d  16011  islssd  16017  islss4  16043  lssacs  16048  lsspropd  16098  islmhmd  16120  lmhmima  16128  lmhmpreima  16129  reslmhm  16133  lspextmo  16137  lsmcl  16160  pj1lmhm  16177  islbs2  16231  issubrngd2  16267  opprdomn  16366  abvn0b  16367  issubassa2  16408  mvrf1  16494  mplsubglem  16503  mplsubrg  16508  mplind  16567  evlslem2  16573  ply1sclf1  16685  prmirredlem  16778  expmhm  16781  expghm  16782  mulgghm2  16791  domnchr  16818  znf1o  16837  zntoslem  16842  znfld  16846  cygznlem3  16855  phlipf  16888  tgclb  17040  mretopd  17161  toponmre  17162  iscldtop  17164  ordtbaslem  17257  ordtbas2  17260  cnt0  17415  haust1  17421  cnhaus  17423  isreg2  17446  dishaus  17451  ordthaus  17453  dfcon2  17487  iuncon  17496  clscon  17498  2ndcomap  17526  dis2ndc  17528  llynlly  17545  restnlly  17550  restlly  17551  islly2  17552  llyidm  17556  nllyidm  17557  hausllycmp  17562  kgentopon  17575  txbas  17604  ptbasin2  17615  ptbasfi  17618  txcnp  17657  txcnmpt  17661  pthaus  17675  tx1stc  17687  xkococnlem  17696  xkococn  17697  cnmpt21  17708  qtoptop2  17736  qtopeu  17753  kqt0lem  17773  isr0  17774  regr1lem2  17777  kqreglem1  17778  kqreglem2  17779  kqnrmlem1  17780  kqnrmlem2  17781  nrmr0reg  17786  reghmph  17830  nrmhmph  17831  txswaphmeo  17842  qtophmeo  17854  fbun  17877  trfbas2  17880  isfil2  17893  infil  17900  trfil2  17924  filssufilg  17948  hausflim  18018  fclsnei  18056  fclsfnflim  18064  flimfnfcls  18065  ptcmplem1  18088  clssubg  18143  tgpconcomp  18147  divstgplem  18155  tsmsfbas  18162  utoptop  18269  iducn  18318  cstucnd  18319  isxmetd  18361  isxmet2d  18362  xmettpos  18384  prdsdsf  18402  prdsmet  18405  ressprdsds  18406  imasdsf1olem  18408  imasf1oxmet  18410  imasf1omet  18411  blfvalps  18418  xmetresbl  18472  metss2  18547  comet  18548  stdbdmet  18551  stdbdmopn  18553  methaus  18555  met2ndci  18557  metustfbasOLD  18600  metustfbas  18601  nrmmetd  18627  subgngp  18681  ngptgp  18682  sranlm  18725  nlmvscnlem1  18727  nlmvscn  18728  nrginvrcn  18732  lssnlm  18741  nghmcn  18784  qtopbaslem  18797  reconn  18864  xmetdcn2  18873  metdscn  18891  metnrm  18897  elcncf1di  18930  cncffvrn  18933  mulc1cncf  18940  cncfco  18942  reparphti  19027  tchcph  19199  ipcnlem1  19204  ipcn  19205  iscfil3  19231  bcthlem5  19286  minveclem3  19335  minveclem7  19341  ovolicc2lem4  19421  dyadmbl  19497  volcn  19503  itg1addlem1  19587  itg1addlem2  19592  itg1addlem4  19594  mbfi1fseqlem1  19610  mbfi1fseqlem3  19612  mbfi1fseqlem4  19613  mbfi1fseqlem5  19614  dvmptfsum  19864  c1liplem1  19885  dvgt0lem2  19892  ftc1a  19926  evlseu  19942  ply1domn  20051  ply1divmo  20063  fta1b  20097  ig1peu  20099  coeeu  20149  plydivalg  20221  aaliou2b  20263  ulmss  20318  ulmcn  20320  efif1olem4  20452  logccv  20559  cvxcl  20828  basellem4  20871  fsumdvdscom  20975  musum  20981  dvdsmulf1o  20984  fsumdvdsmul  20985  dchrelbasd  21028  dchrmulcl  21038  dchrinv  21050  lgsqrlem2  21131  lgsdchr  21137  lgseisenlem2  21139  lgsquadlem1  21143  lgsquadlem2  21144  dchrisumlema  21187  dchrisumlem2  21189  chpdifbndlem2  21253  pntpbnd  21287  pntibndlem3  21291  usgraedgreu  21412  usgraidx2v  21417  isgrp2d  21828  grpoinvf  21833  subgoablo  21904  ghgrplem2  21960  ghablo  21962  nvmf  22132  vacn  22195  nmcvcn  22196  smcnlem  22198  sspg  22232  ssps  22234  sspmlem  22236  0lno  22296  blocni  22311  sspph  22361  ipblnfi  22362  minvecolem7  22390  unopf1o  23424  cnvunop  23426  unoplin  23428  counop  23429  hmopadj2  23449  hmoplin  23450  bralnfn  23456  lnopeq0i  23515  hmops  23528  hmopm  23529  hmopco  23531  lnconi  23541  cnlnadjlem2  23576  adjmul  23600  adjadd  23601  cdjreui  23940  disjxpin  24033  off2  24059  xrofsup  24131  kerf1hrm  24267  pstmxmet  24297  ofcf  24491  sibfof  24659  erdszelem4  24885  erdszelem9  24890  erdsze2lem2  24895  cnpcon  24922  pconcon  24923  txpcon  24924  ptpcon  24925  cvxpcon  24934  cvxscon  24935  iccllyscon  24942  cvmseu  24968  cvmliftmo  24976  cvmlift2lem5  24999  cvmlift2lem9  25003  fprodser  25280  fprod2dlem  25309  fprodcom2  25313  brbtwn2  25849  axlowdimlem15  25900  axcontlem2  25909  axcontlem10  25917  segconeu  25950  onsuct0  26196  heicant  26253  mblfinlem2  26256  ftc1anc  26302  fnessref  26387  neibastop1  26402  filnetlem3  26423  sdclem1  26461  isbnd3  26507  prdsbnd  26516  ismtycnv  26525  ismtyhmeolem  26527  ismtyres  26531  bfplem1  26545  bfplem2  26546  bfp  26547  rrnmet  26552  ismrer1  26561  iccbnd  26563  grpokerinj  26574  isdrngo2  26588  rngogrphom  26601  rngohomco  26604  rngoisocnv  26611  iscringd  26623  erprt  26736  nacsfix  26780  rmxypairf1o  26988  wepwsolem  27130  dnnumch3  27136  fnwe2  27142  dsmmlss  27201  uvcf1  27232  frlmlbs  27240  lindff1  27281  lindfrn  27282  f1lindf  27283  mpaaeu  27346  issubmd  27374  mamucl  27447  mamudiagcl  27448  mamulid  27449  mamurid  27450  mamuass  27451  mamudi  27452  mamudir  27453  mamuvs1  27454  mamuvs2  27455  idomsubgmo  27505  mon1psubm  27516  deg1mhm  27517  dmmpt2g  27973  otsndisj  28080  otiunsndisj  28081  otiunsndisjX  28082  cshwsdisj  28319  2spotiundisj  28525  2spotmdisj  28531  lfl0f  29941  lkrlss  29967  lshpsmreu  29981  linepsubN  30623  pmapsub  30639  lautcnv  30961  lautco  30968  idltrn  31021  cdleme50f1  31414  cdleme50laut  31418  istendod  31633  dihf11  32139  dih1dimatlem  32201  lcfl7N  32373  lcfrlem9  32422  mapd1o  32520  hdmapf1oN  32740  hgmapf1oN  32778
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 1627  ax-9 1667  ax-8 1688  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555  df-ral 2712
  Copyright terms: Public domain W3C validator