Theorem ralrimivva 3156

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	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝜓)

Assertion

Ref	Expression
ralrimivva	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Distinct variable groups:   𝜑,𝑥,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem ralrimivva

Step	Hyp	Ref	Expression
1		ralrimivva.1	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝜓)
2	1	ex 416	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓))
3	2	ralrimivv 3155	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ∀wral 3106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911

This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3111

This theorem is referenced by:  disjord  5018  disjxiun  5027  otsndisj  5374  otiunsndisj  5375  swopo  5448  issod  5470  reuop  6112  fcof1  7021  fliftfund  7045  isof1oidb  7056  isof1oopb  7057  soisores  7059  soisoi  7060  isocnv  7062  f1oiso  7083  oveqrspc2v  7162  oprres  7296  caovclg  7320  caovcomg  7323  off  7404  caofrss  7422  caonncan  7427  dmmpog  7755  fnmpoovd  7765  fmpoco  7773  fsplitfpar  7797  poxp  7805  fvmpocurryd  7920  smo11  7984  smoiso2  7989  omsmo  8264  qsdisj2  8358  eroprf  8378  dom2lem  8532  omxpenlem  8601  xpf1o  8663  unxpdomlem3  8708  fofinf1o  8783  dffi3  8879  supmo  8900  infmo  8943  inf3lem6  9080  cantnf  9140  rankxplim  9292  fseqenlem1  9435  fodomacn  9467  iunfictbso  9525  cofsmo  9680  infpssrlem5  9718  enfin2i  9732  fin23lem23  9737  fin23lem27  9739  fin23lem28  9751  compssiso  9785  ltordlem  11154  cju  11621  axdc4uzlem  13346  seqcaopr2  13402  seqhomo  13413  wrd2ind  14076  cshf1  14163  s3sndisj  14318  s3iunsndisj  14319  climcn2  14941  addcn2  14942  mulcn2  14944  o1of2  14961  isercolllem1  15013  fsum2dlem  15117  fsumcom2  15121  fprodser  15295  fprod2dlem  15326  fprodcom2  15330  isprm6  16048  crth  16105  eulerthlem2  16109  vdwlem12  16318  cshwsdisj  16424  imasaddfnlem  16793  imasvscafn  16802  mreexexd  16911  iscatd  16936  oppccomfpropd  16989  isofn  17037  sectmon  17044  ssctr  17087  ssceq  17088  catsubcat  17101  issubc3  17111  fullsubc  17112  fullresc  17113  isfuncd  17127  idfucl  17143  cofucl  17150  funcres2b  17159  fulloppc  17184  fthoppc  17185  idffth  17195  cofull  17196  cofth  17197  ressffth  17200  setcmon  17339  setcepi  17340  resssetc  17344  resscatc  17357  catciso  17359  fthestrcsetc  17392  fullestrcsetc  17393  embedsetcestrclem  17399  fthsetcestrc  17407  fullsetcestrc  17408  evlfcl  17464  uncfcurf  17481  hofcl  17501  yonedalem3  17522  yonedainv  17523  yonffthlem  17524  yoniso  17527  isdrs2  17541  isposd  17557  pospropd  17736  poslubmo  17748  posglbmo  17749  mgmplusf  17854  issstrmgm  17855  opifismgm  17861  ismndd  17925  mndpropd  17928  issubmnd  17930  mndinvmod  17933  mhmpropd  17954  idmhm  17957  mhmf1o  17958  issubmd  17963  mndissubm  17964  0mhm  17976  resmhm  17977  resmhm2  17978  resmhm2b  17979  mhmco  17980  submacs  17983  prdspjmhm  17985  pwsdiagmhm  17987  pwsco1mhm  17988  pwsco2mhm  17989  gsumwspan  18003  frmdsssubm  18018  frmdup1  18021  grpsubf  18170  dfgrp3  18190  mhmmnd  18213  mhmfmhm  18214  issubg4  18290  grpissubg  18291  isnsg3  18304  nsgacs  18306  0nsg  18313  nsgid  18314  cycsubmcom  18339  isghmd  18359  ghmmhm  18360  idghm  18365  ghmnsgima  18374  ghmnsgpreima  18375  ghmf1  18379  ghmf1o  18380  gaid  18421  subgga  18422  gass  18423  gasubg  18424  cntzsubm  18458  cntrsubgnsg  18463  lactghmga  18525  symgfixf1  18557  odf1  18681  sylow1lem2  18716  sylow2blem2  18738  sylow3lem1  18744  lsmssv  18760  smndlsmidm  18773  lsmidmOLD  18781  pj1eu  18814  efglem  18834  efgtf  18840  efgred  18866  efgredeu  18870  frgpmhm  18883  frgpuptf  18888  frgpuplem  18890  mulgmhm  18941  ghmcmn  18945  invghm  18947  ablnsg  18960  cygabl  19003  gsum2d2lem  19086  gsum2d2  19087  gsumcom2  19088  dprd2d2  19159  ablfaclem2  19201  srgfcl  19258  srglmhm  19278  srgrmhm  19279  isrhm2d  19476  kerf1ghm  19491  issubrg2  19548  subrgint  19550  primefld  19577  islmodd  19633  lmodscaf  19649  lmodprop2d  19689  islssd  19700  islss4  19727  lssacs  19732  lsspropd  19782  islmhmd  19804  lmhmima  19812  lmhmpreima  19813  reslmhm  19817  lspextmo  19821  lsmcl  19848  pj1lmhm  19865  islbs2  19919  issubrngd2  19954  opprdomn  20067  abvn0b  20068  expmhm  20160  nn0srg  20161  prmirredlem  20186  expghm  20189  mulgghm2  20190  domnchr  20224  znf1o  20243  zntoslem  20248  znfld  20252  cygznlem3  20261  phlipf  20341  dsmmlss  20433  uvcf1  20481  frlmlbs  20486  lindff1  20509  lindfrn  20510  f1lindf  20511  issubassa2  20578  mvrf1  20663  mplsubglem  20672  mplsubrg  20678  mplcoe5lem  20707  mplcoe2  20709  mplind  20741  evlslem2  20751  evlseu  20755  mhplss  20803  ply1sclf1  20918  mamucl  21006  mamuass  21007  mamudi  21008  mamudir  21009  mamuvs1  21010  mamuvs2  21011  matbas2d  21028  mamumat1cl  21044  mamulid  21046  mamurid  21047  mat1mhm  21089  dmatid  21100  dmatsubcl  21103  dmatsgrp  21104  dmatmulcl  21105  dmatsrng  21106  dmatcrng  21107  scmatscmiddistr  21113  scmatscm  21118  scmatsgrp  21124  scmatsrng  21125  scmatcrng  21126  scmatsgrp1  21127  scmatsrng1  21128  scmatf1  21136  scmatmhm  21139  mavmul0g  21158  mdet1  21206  mdetunilem9  21225  mdetuni0  21226  mdetmul  21228  madutpos  21247  smadiadetlem4  21274  1elcpmat  21320  cpmatacl  21321  cpmatmcl  21324  mat2pmatf1  21334  mat2pmatmul  21336  mat2pmat1  21337  mat2pmatlin  21340  m2cpm  21346  m2cpminvid  21358  m2cpminvid2  21360  decpmatmul  21377  pmatcollpw1  21381  monmatcollpw  21384  pmatcollpw  21386  pmatcollpw3lem  21388  pmatcollpwscmatlem2  21395  pm2mpf1  21404  mp2pm2mplem4  21414  pm2mpmhmlem2  21424  chp0mat  21451  chpidmat  21452  tgclb  21575  mretopd  21697  toponmre  21698  iscldtop  21700  ordtbaslem  21793  ordtbas2  21796  cnt0  21951  haust1  21957  cnhaus  21959  isreg2  21982  dishaus  21987  ordthaus  21989  dfconn2  22024  iunconn  22033  clsconn  22035  2ndcomap  22063  dis2ndc  22065  llynlly  22082  restnlly  22087  restlly  22088  islly2  22089  llyidm  22093  nllyidm  22094  hausllycmp  22099  kgentopon  22143  txbas  22172  ptbasin2  22183  ptbasfi  22186  txcnp  22225  txcnmpt  22229  pthaus  22243  tx1stc  22255  xkococnlem  22264  xkococn  22265  cnmpt21  22276  qtoptop2  22304  qtopeu  22321  kqt0lem  22341  isr0  22342  regr1lem2  22345  kqreglem1  22346  kqreglem2  22347  kqnrmlem1  22348  kqnrmlem2  22349  nrmr0reg  22354  reghmph  22398  nrmhmph  22399  txswaphmeo  22410  qtophmeo  22422  fbun  22445  trfbas2  22448  isfil2  22461  infil  22468  trfil2  22492  filssufilg  22516  hausflim  22586  fclsnei  22624  fclsfnflim  22632  flimfnfcls  22633  ptcmplem1  22657  clssubg  22714  tgpconncomp  22718  qustgplem  22726  tsmsfbas  22733  utoptop  22840  iducn  22889  cstucnd  22890  isxmetd  22933  isxmet2d  22934  xmettpos  22956  prdsdsf  22974  prdsmet  22977  ressprdsds  22978  imasdsf1olem  22980  imasf1oxmet  22982  imasf1omet  22983  blfvalps  22990  xmetresbl  23044  metss2  23119  comet  23120  stdbdmet  23123  stdbdmopn  23125  methaus  23127  met2ndci  23129  metustfbas  23164  nrmmetd  23181  subgngp  23241  ngptgp  23242  sranlm  23290  nlmvscnlem1  23292  nlmvscn  23293  nrginvrcn  23298  lssnlm  23307  nghmcn  23351  qtopbaslem  23364  reconn  23433  xmetdcn2  23442  metdscn  23461  metnrm  23467  elcncf1di  23500  cncffvrn  23503  mulc1cncf  23510  cncfco  23512  reparphti  23602  isncvsngpd  23755  tcphcph  23841  ipcnlem1  23849  ipcn  23850  iscfil3  23877  bcthlem5  23932  rrxmet  24012  minveclem3  24033  minveclem7  24039  ovolicc2lem4  24124  dyadmbl  24204  volcn  24210  itg1addlem1  24296  itg1addlem2  24301  itg1addlem4  24303  mbfi1fseqlem1  24319  mbfi1fseqlem3  24321  mbfi1fseqlem4  24322  mbfi1fseqlem5  24323  dvmptfsum  24578  c1liplem1  24599  dvgt0lem2  24606  ftc1a  24640  ply1domn  24724  ply1divmo  24736  fta1b  24770  ig1peu  24772  coeeu  24822  plydivalg  24895  aaliou2b  24937  ulmss  24992  ulmcn  24994  efif1olem4  25137  efsubm  25143  logccv  25254  logbmpt  25374  logbfval  25376  cvxcl  25570  basellem4  25669  fsumdvdscom  25770  musum  25776  dvdsmulf1o  25779  fsumdvdsmul  25780  dchrelbasd  25823  dchrmulcl  25833  dchrinv  25845  lgsqrlem2  25931  lgsdchr  25939  lgseisenlem2  25960  lgsquadlem1  25964  lgsquadlem2  25965  2sqreulem4  26038  dchrisumlema  26072  dchrisumlem2  26074  chpdifbndlem2  26138  pntpbnd  26172  pntibndlem3  26176  axtgcont  26263  tgjustc1  26269  tgjustc2  26270  iscgrglt  26308  ercgrg  26311  idmot  26331  motco  26334  cnvmot  26335  motcgrg  26338  tgisline  26421  tghilberti2  26432  mirreu3  26448  mirmot  26469  ragperp  26511  foot  26516  mideu  26532  midf  26570  lmimot  26592  trgcopyeu  26600  f1otrgds  26663  f1otrg  26665  f1otrge  26666  xmstrkgc  26680  brbtwn2  26699  axlowdimlem15  26750  axcontlem2  26759  axcontlem10  26767  eengtrkg  26780  eengtrkge  26781  numedglnl  26937  usgredgreu  27008  uspgredg2vtxeu  27010  uspgredg2v  27014  usgredg2v  27017  wlkswwlksf1o  27665  wwlksnextinj  27685  clwlkclwwlkf1  27795  clwwlkf1  27834  frcond4  28055  frgrncvvdeqlem8  28091  frgrncvvdeq  28094  frgrwopreglem4  28100  numclwwlk1lem2f1  28142  grpoinvf  28315  nvmf  28428  vacn  28477  nmcvcn  28478  smcnlem  28480  sspg  28511  ssps  28513  sspmlem  28515  0lno  28573  blocni  28588  ipblnfi  28638  minvecolem7  28666  unopf1o  29699  cnvunop  29701  unoplin  29703  counop  29704  hmopadj2  29724  hmoplin  29725  bralnfn  29731  lnopeq0i  29790  hmops  29803  hmopm  29804  hmopco  29806  lnconi  29816  cnlnadjlem2  29851  adjmul  29875  adjadd  29876  cdjreui  30215  disjxpin  30351  off2  30402  2ndresdju  30411  fnpreimac  30434  suppovss  30443  f1od2  30483  xrofsup  30518  s3f1  30649  ccatf1  30651  swrdf1  30656  odutos  30676  dfmgc2lem  30703  dfmgc2  30704  pwrssmgc  30706  abliso  30730  symgcntz  30779  tocyccntz  30836  archiabllem1  30872  archiabllem2  30876  suborng  30939  xrge0slmod  30968  intlidl  31010  rhmpreimaidl  31011  idlinsubrg  31016  rhmimaidl  31017  prmidl2  31024  idlmulssprm  31025  isprmidlc  31031  rhmpreimaprmidl  31035  qsidomlem1  31036  qsidomlem2  31037  mxidlprm  31048  ssmxidllem  31049  lindsun  31109  fedgmullem1  31113  fedgmullem2  31114  fedgmul  31115  1smat1  31157  submateq  31162  madjusmdetlem3  31182  zart0  31232  pstmxmet  31250  ofcf  31472  ldgenpisys  31535  rossros  31549  inelcarsg  31679  sibfof  31708  sitmf  31720  hgt750lemb  32037  erdszelem4  32554  erdszelem9  32559  erdsze2lem2  32564  cnpconn  32590  pconnconn  32591  txpconn  32592  ptpconn  32593  cvxpconn  32602  cvxsconn  32603  iccllysconn  32610  cvmseu  32636  cvmliftmo  32644  cvmlift2lem5  32667  cvmlift2lem9  32671  mrsubff1  32874  elmrsubrn  32880  mrsubco  32881  msubff1  32916  mvhf1  32919  sslttr  33381  segconeu  33585  fnessref  33818  neibastop1  33820  filnetlem3  33841  onsuct0  33902  unblimceq0lem  33958  unbdqndv2  33963  knoppndv  33986  irrdiff  34740  uncf  35036  fin2so  35044  lindsadd  35050  poimirlem4  35061  poimirlem13  35070  poimirlem14  35071  poimirlem26  35083  heicant  35092  mblfinlem2  35095  ftc1anc  35138  sdclem1  35181  isbnd3  35222  prdsbnd  35231  ismtycnv  35240  ismtyhmeolem  35242  ismtyres  35246  bfplem1  35260  bfplem2  35261  bfp  35262  rrnmet  35267  ismrer1  35276  iccbnd  35278  grpokerinj  35331  isdrngo2  35396  rngogrphom  35409  rngohomco  35412  rngoisocnv  35419  iscringd  35436  erprt  36169  lfl0f  36365  lkrlss  36391  lshpsmreu  36405  linepsubN  37048  pmapsub  37064  lautcnv  37386  lautco  37393  idltrn  37446  cdleme50f1  37839  cdleme50laut  37843  istendod  38058  dihf11  38563  dih1dimatlem  38625  lcfl7N  38797  lcfrlem9  38846  mapd1o  38944  hdmapf1oN  39161  hgmapf1oN  39199  qsalrel  39420  fsuppind  39456  sn-negex12  39553  nacsfix  39653  rmxypairf1o  39852  wepwsolem  39986  dnnumch3  39991  fnwe2  39997  mpaaeu  40094  idomsubgmo  40142  mon1psubm  40150  deg1mhm  40151  isotone1  40751  isotone2  40752  mnringmulrcld  40936  disjxp1  41703  disjf1  41809  wessf1ornlem  41811  projf1o  41825  sumnnodd  42272  lptioo2  42273  lptioo1  42274  cncfshift  42516  cncfperiod  42521  dvnprodlem1  42588  fourierdlem42  42791  nnfoctbdjlem  43094  isomennd  43170  smflimlem6  43409  otiunsndisjX  43835  imasetpreimafvbijlemf1  43921  iccpartgt  43944  icceuelpart  43953  ichnreuop  43989  sprsymrelfolem2  44010  sprsymrelf  44012  prproropf1o  44024  reupr  44039  reuopreuprim  44043  isomuspgrlem2c  44348  isomuspgr  44352  ismgmd  44396  mgmhmpropd  44405  mgmhmf1o  44407  idmgmhm  44408  issubmgm2  44410  rabsubmgmd  44411  resmgmhm  44418  resmgmhm2  44419  resmgmhm2b  44420  mgmhmco  44421  submgmacs  44424  opmpoismgm  44427  mgmplusgiopALT  44454  isrnghm2d  44525  c0mgm  44533  c0mhm  44534  lidlmmgm  44549  2zlidl  44558  rnghmsscmap2  44597  rnghmsscmap  44598  rnghmsubcsetclem2  44600  rhmsscmap2  44643  rhmsscmap  44644  rhmsubcsetclem2  44646  rhmsscrnghm  44650  rhmsubcrngclem2  44652  srhmsubc  44700  fldhmsubc  44708  rhmsubc  44714  srhmsubcALTV  44718  fldhmsubcALTV  44726  rhmsubcALTV  44732  lindslinindsimp1  44866  1arymaptf1  45056  2arymaptf1  45067