Theorem ralrimivva 3178

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 412	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓))
3	2	ralrimivv 3176	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3045

This theorem is referenced by:  disjord  5091  disjxiun  5099  otsndisj  5474  otiunsndisj  5475  swopo  5550  issod  5574  reuop  6254  fcof1  7244  fliftfund  7270  isof1oidb  7281  isof1oopb  7282  soisores  7284  soisoi  7285  isocnv  7287  f1oiso  7308  oveqrspc2v  7396  oprres  7537  caovclg  7561  caovcomg  7564  off  7651  coof  7657  caofidlcan  7671  caofrss  7672  caonncan  7677  dmmpog  8032  fnmpoovd  8043  fmpoco  8051  fsplitfpar  8074  poxp  8084  fvmpocurryd  8227  smo11  8310  smoiso2  8315  omsmo  8599  nnasmo  8604  coflton  8612  qsdisj2  8745  eroprf  8765  dom2lem  8940  omxpenlem  9019  xpf1o  9080  unxpdomlem3  9175  fofinf1o  9259  dffi3  9358  supmo  9379  infmo  9424  inf3lem6  9562  cantnf  9622  rankxplim  9808  fseqenlem1  9953  fodomacn  9985  iunfictbso  10043  cofsmo  10198  infpssrlem5  10236  enfin2i  10250  fin23lem23  10255  fin23lem27  10257  fin23lem28  10269  compssiso  10303  ltordlem  11679  cju  12158  axdc4uzlem  13924  seqcaopr2  13979  seqhomo  13990  wrd2ind  14664  cshf1  14751  s3sndisj  14909  s3iunsndisj  14910  climcn2  15535  addcn2  15536  mulcn2  15538  o1of2  15555  isercolllem1  15607  fsum2dlem  15712  fsumcom2  15716  fprodser  15891  fprod2dlem  15922  fprodcom2  15926  isprm6  16660  crth  16724  eulerthlem2  16728  vdwlem12  16939  cshwsdisj  17045  imasaddfnlem  17467  imasvscafn  17476  mreexexd  17589  iscatd  17614  oppccomfpropd  17668  isofn  17717  sectmon  17724  ssctr  17767  ssceq  17768  catsubcat  17781  issubc3  17791  fullsubc  17792  fullresc  17793  isfuncd  17807  idfucl  17823  cofucl  17830  funcres2b  17839  fulloppc  17866  fthoppc  17867  idffth  17877  cofull  17878  cofth  17879  ressffth  17882  setcmon  18029  setcepi  18030  resssetc  18034  resscatc  18051  catciso  18053  fthestrcsetc  18091  fullestrcsetc  18092  embedsetcestrclem  18098  fthsetcestrc  18106  fullsetcestrc  18107  evlfcl  18163  uncfcurf  18180  hofcl  18200  yonedalem3  18221  yonedainv  18222  yonffthlem  18223  yoniso  18226  isdrs2  18247  isposd  18263  pospropd  18266  poslubmo  18350  posglbmo  18351  mgmplusf  18559  ismgmd  18561  issstrmgm  18562  opifismgm  18568  mgmhmpropd  18607  mgmhmf1o  18609  idmgmhm  18610  issubmgm2  18612  rabsubmgmd  18613  resmgmhm  18620  resmgmhm2  18621  resmgmhm2b  18622  mgmhmco  18623  submgmacs  18626  issgrpd  18639  sgrppropd  18640  ismndd  18665  mndpropd  18668  issubmnd  18670  mndinvmod  18673  ismhmd  18695  mhmpropd  18701  idmhm  18704  mhmf1o  18705  issubmd  18715  mndissubm  18716  0mhm  18728  resmhm  18729  resmhm2  18730  resmhm2b  18731  mhmco  18732  submacs  18736  prdspjmhm  18738  pwsdiagmhm  18740  pwsco1mhm  18741  pwsco2mhm  18742  gsumwspan  18755  frmdsssubm  18770  frmdup1  18773  grpsubf  18933  dfgrp3  18953  mhmmnd  18978  mhmfmhm  18979  issubg4  19059  grpissubg  19060  isnsg3  19074  nsgacs  19076  0nsg  19083  nsgid  19084  qus0subgadd  19113  cycsubmcom  19118  isghmd  19139  ghmmhm  19140  idghm  19145  ghmnsgima  19154  ghmnsgpreima  19155  ghmf1  19160  kerf1ghm  19161  ghmf1o  19162  gaid  19213  subgga  19214  gass  19215  gasubg  19216  cntzsgrpcl  19248  cntzsubm  19252  cntrsubgnsg  19257  lactghmga  19319  symgfixf1  19351  odf1  19476  sylow1lem2  19513  sylow2blem2  19535  sylow3lem1  19541  lsmssv  19557  smndlsmidm  19570  pj1eu  19610  efglem  19630  efgtf  19636  efgred  19662  efgredeu  19666  frgpmhm  19679  frgpuptf  19684  frgpuplem  19686  mulgmhm  19741  ghmcmn  19745  invghm  19747  ablnsg  19761  imasabl  19790  cygabl  19805  gsum2d2lem  19887  gsum2d2  19888  gsumcom2  19889  dprd2d2  19960  ablfaclem2  20002  srgfcl  20116  srgcom4lem  20133  srglmhm  20141  srgrmhm  20142  ringcomlem  20199  isrnghm2d  20370  c0mgm  20379  c0mhm  20380  isrhm2d  20407  subrngringnsg  20473  issubrng2  20478  subrngint  20480  issubrg2  20512  subrgint  20515  rnghmsscmap2  20549  rnghmsscmap  20550  rnghmsubcsetclem2  20552  rhmsscmap2  20578  rhmsscmap  20579  rhmsubcsetclem2  20581  rhmsscrnghm  20585  rhmsubcrngclem2  20587  srhmsubc  20600  rhmsubc  20609  fldhmsubc  20705  primefld  20725  abvn0b  20756  suborng  20796  islmodd  20804  lmodscaf  20822  lmodprop2d  20862  islssd  20873  islss4  20900  lssacs  20905  lsspropd  20956  islmhmd  20978  lmhmima  20986  lmhmpreima  20987  reslmhm  20991  lspextmo  20995  lsmcl  21022  pj1lmhm  21039  islbs2  21096  issubrgd  21128  dflidl2rng  21160  rnglidlmmgm  21187  rhmpreimaidl  21219  rngqiprnglin  21244  expmhm  21378  nn0srg  21379  prmirredlem  21414  expghm  21417  mulgghm2  21418  domnchr  21474  znf1o  21493  zntoslem  21498  znfld  21502  cygznlem3  21511  phlipf  21594  dsmmlss  21686  uvcf1  21734  frlmlbs  21739  lindff1  21762  lindfrn  21763  f1lindf  21764  issubassa2  21834  mvrf1  21928  mplsubglem  21941  mplsubrg  21947  mplcoe5lem  21979  mplcoe2  21981  mplind  22010  evlslem2  22019  evlseu  22023  mhplss  22075  ply1sclf1  22208  evls1maplmhm  22297  mamucl  22321  mamuass  22322  mamudi  22323  mamudir  22324  mamuvs1  22325  mamuvs2  22326  matbas2d  22343  mamumat1cl  22359  mamulid  22361  mamurid  22362  mat1mhm  22404  dmatid  22415  dmatsubcl  22418  dmatsgrp  22419  dmatmulcl  22420  dmatsrng  22421  dmatcrng  22422  scmatscmiddistr  22428  scmatscm  22433  scmatsgrp  22439  scmatsrng  22440  scmatcrng  22441  scmatsgrp1  22442  scmatsrng1  22443  scmatf1  22451  scmatmhm  22454  mavmul0g  22473  mdet1  22521  mdetunilem9  22540  mdetuni0  22541  mdetmul  22543  madutpos  22562  smadiadetlem4  22589  1elcpmat  22635  cpmatacl  22636  cpmatmcl  22639  mat2pmatf1  22649  mat2pmatmul  22651  mat2pmat1  22652  mat2pmatlin  22655  m2cpm  22661  m2cpminvid  22673  m2cpminvid2  22675  decpmatmul  22692  pmatcollpw1  22696  monmatcollpw  22699  pmatcollpw  22701  pmatcollpw3lem  22703  pmatcollpwscmatlem2  22710  pm2mpf1  22719  mp2pm2mplem4  22729  pm2mpmhmlem2  22739  chp0mat  22766  chpidmat  22767  tgclb  22890  mretopd  23012  toponmre  23013  iscldtop  23015  ordtbaslem  23108  ordtbas2  23111  cnt0  23266  haust1  23272  cnhaus  23274  isreg2  23297  dishaus  23302  ordthaus  23304  dfconn2  23339  iunconn  23348  clsconn  23350  2ndcomap  23378  dis2ndc  23380  llynlly  23397  restnlly  23402  restlly  23403  islly2  23404  llyidm  23408  nllyidm  23409  hausllycmp  23414  kgentopon  23458  txbas  23487  ptbasin2  23498  ptbasfi  23501  txcnp  23540  txcnmpt  23544  pthaus  23558  tx1stc  23570  xkococnlem  23579  xkococn  23580  cnmpt21  23591  qtoptop2  23619  qtopeu  23636  kqt0lem  23656  isr0  23657  regr1lem2  23660  kqreglem1  23661  kqreglem2  23662  kqnrmlem1  23663  kqnrmlem2  23664  nrmr0reg  23669  reghmph  23713  nrmhmph  23714  txswaphmeo  23725  qtophmeo  23737  fbun  23760  trfbas2  23763  isfil2  23776  infil  23783  trfil2  23807  filssufilg  23831  hausflim  23901  fclsnei  23939  fclsfnflim  23947  flimfnfcls  23948  ptcmplem1  23972  clssubg  24029  tgpconncomp  24033  qustgplem  24041  tsmsfbas  24048  utoptop  24155  iducn  24203  cstucnd  24204  isxmetd  24247  isxmet2d  24248  xmettpos  24270  prdsdsf  24288  prdsmet  24291  ressprdsds  24292  imasdsf1olem  24294  imasf1oxmet  24296  imasf1omet  24297  blfvalps  24304  xmetresbl  24358  metss2  24433  comet  24434  stdbdmet  24437  stdbdmopn  24439  methaus  24441  met2ndci  24443  metustfbas  24478  nrmmetd  24495  subgngp  24556  ngptgp  24557  sranlm  24605  nlmvscnlem1  24607  nlmvscn  24608  nrginvrcn  24613  lssnlm  24622  nghmcn  24666  qtopbaslem  24679  reconn  24750  xmetdcn2  24759  metdscn  24778  metnrm  24784  elcncf1di  24821  cncfcdm  24824  mulc1cncf  24831  cncfco  24833  reparphti  24929  reparphtiOLD  24930  isncvsngpd  25083  tcphcph  25170  ipcnlem1  25178  ipcn  25179  iscfil3  25206  bcthlem5  25261  rrxmet  25341  minveclem3  25362  minveclem7  25368  ovolicc2lem4  25454  dyadmbl  25534  volcn  25540  itg1addlem1  25626  itg1addlem2  25631  itg1addlem4  25633  mbfi1fseqlem1  25649  mbfi1fseqlem3  25651  mbfi1fseqlem4  25652  mbfi1fseqlem5  25653  dvmptfsum  25912  c1liplem1  25934  dvgt0lem2  25941  ftc1a  25977  ply1domn  26062  ply1divmo  26074  fta1b  26110  ig1peu  26113  coeeu  26163  plydivalg  26240  aaliou2b  26282  ulmss  26339  ulmcn  26341  efif1olem4  26487  efsubm  26493  logccv  26605  logbmpt  26731  logbfval  26733  cvxcl  26928  basellem4  27027  fsumdvdscom  27128  musum  27134  mpodvdsmulf1o  27137  fsumdvdsmul  27138  dvdsmulf1o  27139  fsumdvdsmulOLD  27140  dchrelbasd  27183  dchrmulcl  27193  dchrinv  27205  lgsqrlem2  27291  lgsdchr  27299  lgseisenlem2  27320  lgsquadlem1  27324  lgsquadlem2  27325  2sqreulem4  27398  dchrisumlema  27432  dchrisumlem2  27434  chpdifbndlem2  27498  pntpbnd  27532  pntibndlem3  27536  ssltd  27737  oldbday  27850  addsprop  27923  mulscutlem  28074  divsmo  28127  om2noseqf1o  28235  om2noseqiso  28236  axtgcont  28449  tgjustc1  28455  tgjustc2  28456  iscgrglt  28494  ercgrg  28497  idmot  28517  motco  28520  cnvmot  28521  motcgrg  28524  tgisline  28607  tghilberti2  28618  mirreu3  28634  mirmot  28655  ragperp  28697  foot  28702  mideu  28718  midf  28756  lmimot  28778  trgcopyeu  28786  f1otrgds  28849  f1otrg  28851  f1otrge  28852  xmstrkgc  28866  brbtwn2  28885  axlowdimlem15  28936  axcontlem2  28945  axcontlem10  28953  eengtrkg  28966  eengtrkge  28967  numedglnl  29124  usgredgreu  29198  uspgredg2vtxeu  29200  uspgredg2v  29204  usgredg2v  29207  wlkswwlksf1o  29859  wwlksnextinj  29879  clwlkclwwlkf1  29989  clwwlkf1  30028  frcond4  30249  frgrncvvdeqlem8  30285  frgrncvvdeq  30288  frgrwopreglem4  30294  numclwwlk1lem2f1  30336  nrt2irr  30452  grpoinvf  30511  nvmf  30624  vacn  30673  nmcvcn  30674  smcnlem  30676  sspg  30707  ssps  30709  sspmlem  30711  0lno  30769  blocni  30784  ipblnfi  30834  minvecolem7  30862  unopf1o  31895  cnvunop  31897  unoplin  31899  counop  31900  hmopadj2  31920  hmoplin  31921  bralnfn  31927  lnopeq0i  31986  hmops  31999  hmopm  32000  hmopco  32002  lnconi  32012  cnlnadjlem2  32047  adjmul  32071  adjadd  32072  cdjreui  32411  disjxpin  32567  off2  32615  2ndresdju  32623  fnpreimac  32645  suppovss  32654  f1od2  32694  xrofsup  32740  s3f1  32918  ccatf1  32920  swrdf1  32928  odutos  32940  dfmgc2lem  32967  dfmgc2  32968  pwrssmgc  32972  mgcf1o  32975  mndlactf1  33010  mndractf1  33012  abliso  33020  symgcntz  33057  tocyccntz  33116  conjga  33142  archiabllem1  33162  archiabllem2  33166  urpropd  33199  elrgspnlem2  33210  rlocf1  33240  rrgsubm  33250  subrdom  33251  xrge0slmod  33312  nsgmgc  33376  intlidl  33384  idlinsubrg  33395  rhmimaidl  33396  prmidl2  33405  idlmulssprm  33406  isprmidlc  33411  rhmpreimaprmidl  33415  qsidomlem1  33416  qsidomlem2  33417  ssdifidllem  33420  ssdifidlprm  33422  mxidlprm  33434  mxidlirredi  33435  ssmxidllem  33437  rsprprmprmidl  33486  rsprprmprmidlb  33487  rprmirred  33495  rprmirredb  33496  1arithufdlem4  33511  ply1degltdimlem  33611  ply1degltdim  33612  lindsun  33614  fedgmullem1  33618  fedgmullem2  33619  fedgmul  33620  lactlmhm  33623  assalactf1o  33624  minplyirred  33694  constrsdrg  33758  1smat1  33787  submateq  33792  madjusmdetlem3  33812  zart0  33862  pstmxmet  33880  ofcf  34086  ldgenpisys  34149  rossros  34163  inelcarsg  34295  sibfof  34324  sitmf  34336  hgt750lemb  34640  erdszelem4  35174  erdszelem9  35179  erdsze2lem2  35184  cnpconn  35210  pconnconn  35211  txpconn  35212  ptpconn  35213  cvxpconn  35222  cvxsconn  35223  iccllysconn  35230  cvmseu  35256  cvmliftmo  35264  cvmlift2lem5  35287  cvmlift2lem9  35291  mrsubff1  35494  elmrsubrn  35500  mrsubco  35501  msubff1  35536  mvhf1  35539  r1peuqusdeg1  35623  segconeu  35992  fnessref  36338  neibastop1  36340  filnetlem3  36361  onsuct0  36422  weiunlem2  36444  unblimceq0lem  36487  unbdqndv2  36492  knoppndv  36515  irrdiff  37307  uncf  37586  fin2so  37594  lindsadd  37600  poimirlem4  37611  poimirlem13  37620  poimirlem14  37621  poimirlem26  37633  heicant  37642  mblfinlem2  37645  ftc1anc  37688  sdclem1  37730  isbnd3  37771  prdsbnd  37780  ismtycnv  37789  ismtyhmeolem  37791  ismtyres  37795  bfplem1  37809  bfplem2  37810  bfp  37811  rrnmet  37816  ismrer1  37825  iccbnd  37827  grpokerinj  37880  isdrngo2  37945  rngogrphom  37958  rngohomco  37961  rngoisocnv  37968  iscringd  37985  eqvreldisj1  38809  erprt  38859  lfl0f  39055  lkrlss  39081  lshpsmreu  39095  linepsubN  39739  pmapsub  39755  lautcnv  40077  lautco  40084  idltrn  40137  cdleme50f1  40530  cdleme50laut  40534  istendod  40749  dihf11  41254  dih1dimatlem  41316  lcfl7N  41488  lcfrlem9  41537  mapd1o  41635  hdmapf1oN  41852  hgmapf1oN  41890  fmpocos  42215  qsalrel  42221  rediveud  42424  imacrhmcl  42495  evlselv  42568  fsuppind  42571  nacsfix  42693  rmxypairf1o  42893  wepwsolem  43024  dnnumch3  43029  fnwe2  43035  mpaaeu  43132  idomsubgmo  43175  mon1psubm  43181  deg1mhm  43182  isotone1  44030  isotone2  44031  mnringmulrcld  44210  traxext  44960  disjxp1  45056  disjf1  45170  wessf1ornlem  45172  projf1o  45184  sumnnodd  45621  lptioo2  45622  lptioo1  45623  cncfshift  45865  cncfperiod  45870  dvnprodlem1  45937  fourierdlem42  46140  nnfoctbdjlem  46446  isomennd  46522  smflimlem6  46767  fsetsnf1  47046  cfsetsnfsetf1  47053  otiunsndisjX  47273  imasetpreimafvbijlemf1  47398  iccpartgt  47421  icceuelpart  47430  ichnreuop  47466  sprsymrelfolem2  47487  sprsymrelf  47489  prproropf1o  47501  reupr  47516  reuopreuprim  47520  uhgrimprop  47885  isuspgrim0lem  47886  upgrimtrls  47899  gpgprismgr4cycllem11  48088  opmpoismgm  48148  mgmplusgiopALT  48175  2zlidl  48221  rhmsubcALTV  48266  srhmsubcALTV  48306  fldhmsubcALTV  48314  lindslinindsimp1  48439  1arymaptf1  48624  2arymaptf1  48635  eqfnovd  48847  fmpodg  48850  toslat  48963  catprsc  48995  catprsc2  48996  oppcendc  49000  invfn  49012  iinfssclem2  49037  iinfssc  49039  iinfsubc  49040  discsubc  49046  nelsubclem  49049  resccatlem  49055  funchomf  49079  imasubclem2  49087  imaidfu  49092  imasubc  49133  imassc  49135  imasubc3  49138  fthcomf  49139  idfth  49140  cofidfth  49144  upeu2  49154  isnatd  49205  swapfffth  49265  diag1f1  49289  diag2f1  49291  fucoppc  49392  isthincd  49418  isthincd2  49419  oppcthinco  49421  oppcthinendcALT  49423  functhinclem4  49429  functhincfun  49431  thincfth  49434  thincciso  49435  thinccisod  49436  functermc  49490  arweuthinc  49511  arweutermc  49512  diagffth  49520  funcsn  49523  0fucterm  49525