Theorem ralrimivva 3208

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  disjord  5155  disjxiun  5163  otsndisj  5538  otiunsndisj  5539  swopo  5619  issod  5642  reuop  6324  fcof1  7323  fliftfund  7349  isof1oidb  7360  isof1oopb  7361  soisores  7363  soisoi  7364  isocnv  7366  f1oiso  7387  oveqrspc2v  7475  oprres  7618  caovclg  7642  caovcomg  7645  off  7732  coof  7737  caofrss  7751  caonncan  7756  dmmpog  8115  fnmpoovd  8128  fmpoco  8136  fsplitfpar  8159  poxp  8169  fvmpocurryd  8312  smo11  8420  smoiso2  8425  omsmo  8714  nnasmo  8719  coflton  8727  qsdisj2  8853  eroprf  8873  dom2lem  9052  omxpenlem  9139  xpf1o  9205  unxpdomlem3  9315  fofinf1o  9400  dffi3  9500  supmo  9521  infmo  9564  inf3lem6  9702  cantnf  9762  rankxplim  9948  fseqenlem1  10093  fodomacn  10125  iunfictbso  10183  cofsmo  10338  infpssrlem5  10376  enfin2i  10390  fin23lem23  10395  fin23lem27  10397  fin23lem28  10409  compssiso  10443  ltordlem  11815  cju  12289  axdc4uzlem  14034  seqcaopr2  14089  seqhomo  14100  wrd2ind  14771  cshf1  14858  s3sndisj  15016  s3iunsndisj  15017  climcn2  15639  addcn2  15640  mulcn2  15642  o1of2  15659  isercolllem1  15713  fsum2dlem  15818  fsumcom2  15822  fprodser  15997  fprod2dlem  16028  fprodcom2  16032  isprm6  16761  crth  16825  eulerthlem2  16829  vdwlem12  17039  cshwsdisj  17146  imasaddfnlem  17588  imasvscafn  17597  mreexexd  17706  iscatd  17731  oppccomfpropd  17787  isofn  17836  sectmon  17843  ssctr  17886  ssceq  17887  catsubcat  17903  issubc3  17913  fullsubc  17914  fullresc  17915  isfuncd  17929  idfucl  17945  cofucl  17952  funcres2b  17961  fulloppc  17989  fthoppc  17990  idffth  18000  cofull  18001  cofth  18002  ressffth  18005  setcmon  18154  setcepi  18155  resssetc  18159  resscatc  18176  catciso  18178  fthestrcsetc  18219  fullestrcsetc  18220  embedsetcestrclem  18226  fthsetcestrc  18234  fullsetcestrc  18235  evlfcl  18292  uncfcurf  18309  hofcl  18329  yonedalem3  18350  yonedainv  18351  yonffthlem  18352  yoniso  18355  isdrs2  18376  isposd  18393  pospropd  18397  poslubmo  18481  posglbmo  18482  mgmplusf  18688  ismgmd  18690  issstrmgm  18691  opifismgm  18697  mgmhmpropd  18736  mgmhmf1o  18738  idmgmhm  18739  issubmgm2  18741  rabsubmgmd  18742  resmgmhm  18749  resmgmhm2  18750  resmgmhm2b  18751  mgmhmco  18752  submgmacs  18755  issgrpd  18768  sgrppropd  18769  ismndd  18794  mndpropd  18797  issubmnd  18799  mndinvmod  18802  ismhmd  18821  mhmpropd  18827  idmhm  18830  mhmf1o  18831  issubmd  18841  mndissubm  18842  0mhm  18854  resmhm  18855  resmhm2  18856  resmhm2b  18857  mhmco  18858  submacs  18862  prdspjmhm  18864  pwsdiagmhm  18866  pwsco1mhm  18867  pwsco2mhm  18868  gsumwspan  18881  frmdsssubm  18896  frmdup1  18899  grpsubf  19059  dfgrp3  19079  mhmmnd  19104  mhmfmhm  19105  issubg4  19185  grpissubg  19186  isnsg3  19200  nsgacs  19202  0nsg  19209  nsgid  19210  qus0subgadd  19239  cycsubmcom  19244  isghmd  19265  ghmmhm  19266  idghm  19271  ghmnsgima  19280  ghmnsgpreima  19281  ghmf1  19286  kerf1ghm  19287  ghmf1o  19288  gaid  19339  subgga  19340  gass  19341  gasubg  19342  cntzsgrpcl  19374  cntzsubm  19378  cntrsubgnsg  19383  lactghmga  19447  symgfixf1  19479  odf1  19604  sylow1lem2  19641  sylow2blem2  19663  sylow3lem1  19669  lsmssv  19685  smndlsmidm  19698  pj1eu  19738  efglem  19758  efgtf  19764  efgred  19790  efgredeu  19794  frgpmhm  19807  frgpuptf  19812  frgpuplem  19814  mulgmhm  19869  ghmcmn  19873  invghm  19875  ablnsg  19889  imasabl  19918  cygabl  19933  gsum2d2lem  20015  gsum2d2  20016  gsumcom2  20017  dprd2d2  20088  ablfaclem2  20130  srgfcl  20223  srgcom4lem  20240  srglmhm  20248  srgrmhm  20249  ringcomlem  20302  isrnghm2d  20476  c0mgm  20485  c0mhm  20486  isrhm2d  20513  subrngringnsg  20579  issubrng2  20584  subrngint  20586  issubrg2  20620  subrgint  20623  rnghmsscmap2  20651  rnghmsscmap  20652  rnghmsubcsetclem2  20654  rhmsscmap2  20680  rhmsscmap  20681  rhmsubcsetclem2  20683  rhmsscrnghm  20687  rhmsubcrngclem2  20689  srhmsubc  20702  rhmsubc  20711  fldhmsubc  20808  primefld  20828  abvn0b  20859  islmodd  20886  lmodscaf  20904  lmodprop2d  20944  islssd  20956  islss4  20983  lssacs  20988  lsspropd  21039  islmhmd  21061  lmhmima  21069  lmhmpreima  21070  reslmhm  21074  lspextmo  21078  lsmcl  21105  pj1lmhm  21122  islbs2  21179  issubrgd  21219  dflidl2rng  21251  rnglidlmmgm  21278  rhmpreimaidl  21310  rngqiprnglin  21335  expmhm  21477  nn0srg  21478  prmirredlem  21506  expghm  21509  mulgghm2  21510  domnchr  21570  znf1o  21593  zntoslem  21598  znfld  21602  cygznlem3  21611  phlipf  21693  dsmmlss  21787  uvcf1  21835  frlmlbs  21840  lindff1  21863  lindfrn  21864  f1lindf  21865  issubassa2  21935  mvrf1  22029  mplsubglem  22042  mplsubrg  22048  mplcoe5lem  22080  mplcoe2  22082  mplind  22117  evlslem2  22126  evlseu  22130  mhplss  22182  ply1sclf1  22313  evls1maplmhm  22402  mamucl  22426  mamuass  22427  mamudi  22428  mamudir  22429  mamuvs1  22430  mamuvs2  22431  matbas2d  22450  mamumat1cl  22466  mamulid  22468  mamurid  22469  mat1mhm  22511  dmatid  22522  dmatsubcl  22525  dmatsgrp  22526  dmatmulcl  22527  dmatsrng  22528  dmatcrng  22529  scmatscmiddistr  22535  scmatscm  22540  scmatsgrp  22546  scmatsrng  22547  scmatcrng  22548  scmatsgrp1  22549  scmatsrng1  22550  scmatf1  22558  scmatmhm  22561  mavmul0g  22580  mdet1  22628  mdetunilem9  22647  mdetuni0  22648  mdetmul  22650  madutpos  22669  smadiadetlem4  22696  1elcpmat  22742  cpmatacl  22743  cpmatmcl  22746  mat2pmatf1  22756  mat2pmatmul  22758  mat2pmat1  22759  mat2pmatlin  22762  m2cpm  22768  m2cpminvid  22780  m2cpminvid2  22782  decpmatmul  22799  pmatcollpw1  22803  monmatcollpw  22806  pmatcollpw  22808  pmatcollpw3lem  22810  pmatcollpwscmatlem2  22817  pm2mpf1  22826  mp2pm2mplem4  22836  pm2mpmhmlem2  22846  chp0mat  22873  chpidmat  22874  tgclb  22998  mretopd  23121  toponmre  23122  iscldtop  23124  ordtbaslem  23217  ordtbas2  23220  cnt0  23375  haust1  23381  cnhaus  23383  isreg2  23406  dishaus  23411  ordthaus  23413  dfconn2  23448  iunconn  23457  clsconn  23459  2ndcomap  23487  dis2ndc  23489  llynlly  23506  restnlly  23511  restlly  23512  islly2  23513  llyidm  23517  nllyidm  23518  hausllycmp  23523  kgentopon  23567  txbas  23596  ptbasin2  23607  ptbasfi  23610  txcnp  23649  txcnmpt  23653  pthaus  23667  tx1stc  23679  xkococnlem  23688  xkococn  23689  cnmpt21  23700  qtoptop2  23728  qtopeu  23745  kqt0lem  23765  isr0  23766  regr1lem2  23769  kqreglem1  23770  kqreglem2  23771  kqnrmlem1  23772  kqnrmlem2  23773  nrmr0reg  23778  reghmph  23822  nrmhmph  23823  txswaphmeo  23834  qtophmeo  23846  fbun  23869  trfbas2  23872  isfil2  23885  infil  23892  trfil2  23916  filssufilg  23940  hausflim  24010  fclsnei  24048  fclsfnflim  24056  flimfnfcls  24057  ptcmplem1  24081  clssubg  24138  tgpconncomp  24142  qustgplem  24150  tsmsfbas  24157  utoptop  24264  iducn  24313  cstucnd  24314  isxmetd  24357  isxmet2d  24358  xmettpos  24380  prdsdsf  24398  prdsmet  24401  ressprdsds  24402  imasdsf1olem  24404  imasf1oxmet  24406  imasf1omet  24407  blfvalps  24414  xmetresbl  24468  metss2  24546  comet  24547  stdbdmet  24550  stdbdmopn  24552  methaus  24554  met2ndci  24556  metustfbas  24591  nrmmetd  24608  subgngp  24669  ngptgp  24670  sranlm  24726  nlmvscnlem1  24728  nlmvscn  24729  nrginvrcn  24734  lssnlm  24743  nghmcn  24787  qtopbaslem  24800  reconn  24869  xmetdcn2  24878  metdscn  24897  metnrm  24903  elcncf1di  24940  cncfcdm  24943  mulc1cncf  24950  cncfco  24952  reparphti  25048  reparphtiOLD  25049  isncvsngpd  25203  tcphcph  25290  ipcnlem1  25298  ipcn  25299  iscfil3  25326  bcthlem5  25381  rrxmet  25461  minveclem3  25482  minveclem7  25488  ovolicc2lem4  25574  dyadmbl  25654  volcn  25660  itg1addlem1  25746  itg1addlem2  25751  itg1addlem4  25753  itg1addlem4OLD  25754  mbfi1fseqlem1  25770  mbfi1fseqlem3  25772  mbfi1fseqlem4  25773  mbfi1fseqlem5  25774  dvmptfsum  26033  c1liplem1  26055  dvgt0lem2  26062  ftc1a  26098  ply1domn  26183  ply1divmo  26195  fta1b  26231  ig1peu  26234  coeeu  26284  plydivalg  26359  aaliou2b  26401  ulmss  26458  ulmcn  26460  efif1olem4  26605  efsubm  26611  logccv  26723  logbmpt  26849  logbfval  26851  cvxcl  27046  basellem4  27145  fsumdvdscom  27246  musum  27252  mpodvdsmulf1o  27255  fsumdvdsmul  27256  dvdsmulf1o  27257  fsumdvdsmulOLD  27258  dchrelbasd  27301  dchrmulcl  27311  dchrinv  27323  lgsqrlem2  27409  lgsdchr  27417  lgseisenlem2  27438  lgsquadlem1  27442  lgsquadlem2  27443  2sqreulem4  27516  dchrisumlema  27550  dchrisumlem2  27552  chpdifbndlem2  27616  pntpbnd  27650  pntibndlem3  27654  ssltd  27854  oldbday  27957  addsprop  28027  mulscutlem  28175  divsmo  28228  om2noseqf1o  28325  om2noseqiso  28326  axtgcont  28495  tgjustc1  28501  tgjustc2  28502  iscgrglt  28540  ercgrg  28543  idmot  28563  motco  28566  cnvmot  28567  motcgrg  28570  tgisline  28653  tghilberti2  28664  mirreu3  28680  mirmot  28701  ragperp  28743  foot  28748  mideu  28764  midf  28802  lmimot  28824  trgcopyeu  28832  f1otrgds  28895  f1otrg  28897  f1otrge  28898  xmstrkgc  28918  brbtwn2  28938  axlowdimlem15  28989  axcontlem2  28998  axcontlem10  29006  eengtrkg  29019  eengtrkge  29020  numedglnl  29179  usgredgreu  29253  uspgredg2vtxeu  29255  uspgredg2v  29259  usgredg2v  29262  wlkswwlksf1o  29912  wwlksnextinj  29932  clwlkclwwlkf1  30042  clwwlkf1  30081  frcond4  30302  frgrncvvdeqlem8  30338  frgrncvvdeq  30341  frgrwopreglem4  30347  numclwwlk1lem2f1  30389  nrt2irr  30505  grpoinvf  30564  nvmf  30677  vacn  30726  nmcvcn  30727  smcnlem  30729  sspg  30760  ssps  30762  sspmlem  30764  0lno  30822  blocni  30837  ipblnfi  30887  minvecolem7  30915  unopf1o  31948  cnvunop  31950  unoplin  31952  counop  31953  hmopadj2  31973  hmoplin  31974  bralnfn  31980  lnopeq0i  32039  hmops  32052  hmopm  32053  hmopco  32055  lnconi  32065  cnlnadjlem2  32100  adjmul  32124  adjadd  32125  cdjreui  32464  disjxpin  32610  off2  32660  2ndresdju  32667  fnpreimac  32689  suppovss  32697  f1od2  32735  xrofsup  32774  s3f1  32913  ccatf1  32915  swrdf1  32923  odutos  32941  dfmgc2lem  32968  dfmgc2  32969  pwrssmgc  32973  mgcf1o  32976  mndlactf1  33012  mndractf1  33014  abliso  33022  symgcntz  33078  tocyccntz  33137  archiabllem1  33173  archiabllem2  33177  urpropd  33212  rlocf1  33245  rrgsubm  33253  subrdom  33254  suborng  33310  xrge0slmod  33341  nsgmgc  33405  intlidl  33413  idlinsubrg  33424  rhmimaidl  33425  prmidl2  33434  idlmulssprm  33435  isprmidlc  33440  rhmpreimaprmidl  33444  qsidomlem1  33445  qsidomlem2  33446  ssdifidllem  33449  ssdifidlprm  33451  mxidlprm  33463  mxidlirredi  33464  ssmxidllem  33466  rsprprmprmidl  33515  rsprprmprmidlb  33516  rprmirred  33524  rprmirredb  33525  1arithufdlem4  33540  ply1degltdimlem  33635  ply1degltdim  33636  lindsun  33638  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  lactlmhm  33647  assalactf1o  33648  minplyirred  33704  1smat1  33750  submateq  33755  madjusmdetlem3  33775  zart0  33825  pstmxmet  33843  ofcf  34067  ldgenpisys  34130  rossros  34144  inelcarsg  34276  sibfof  34305  sitmf  34317  hgt750lemb  34633  erdszelem4  35162  erdszelem9  35167  erdsze2lem2  35172  cnpconn  35198  pconnconn  35199  txpconn  35200  ptpconn  35201  cvxpconn  35210  cvxsconn  35211  iccllysconn  35218  cvmseu  35244  cvmliftmo  35252  cvmlift2lem5  35275  cvmlift2lem9  35279  mrsubff1  35482  elmrsubrn  35488  mrsubco  35489  msubff1  35524  mvhf1  35527  r1peuqusdeg1  35611  segconeu  35975  fnessref  36323  neibastop1  36325  filnetlem3  36346  onsuct0  36407  weiunlem2  36429  unblimceq0lem  36472  unbdqndv2  36477  knoppndv  36500  irrdiff  37292  uncf  37559  fin2so  37567  lindsadd  37573  poimirlem4  37584  poimirlem13  37593  poimirlem14  37594  poimirlem26  37606  heicant  37615  mblfinlem2  37618  ftc1anc  37661  sdclem1  37703  isbnd3  37744  prdsbnd  37753  ismtycnv  37762  ismtyhmeolem  37764  ismtyres  37768  bfplem1  37782  bfplem2  37783  bfp  37784  rrnmet  37789  ismrer1  37798  iccbnd  37800  grpokerinj  37853  isdrngo2  37918  rngogrphom  37931  rngohomco  37934  rngoisocnv  37941  iscringd  37958  eqvreldisj1  38780  erprt  38829  lfl0f  39025  lkrlss  39051  lshpsmreu  39065  linepsubN  39709  pmapsub  39725  lautcnv  40047  lautco  40054  idltrn  40107  cdleme50f1  40500  cdleme50laut  40504  istendod  40719  dihf11  41224  dih1dimatlem  41286  lcfl7N  41458  lcfrlem9  41507  mapd1o  41605  hdmapf1oN  41822  hgmapf1oN  41860  fmpocos  42229  qsalrel  42235  imacrhmcl  42469  evlselv  42542  fsuppind  42545  nacsfix  42668  rmxypairf1o  42868  wepwsolem  42999  dnnumch3  43004  fnwe2  43010  mpaaeu  43107  idomsubgmo  43154  mon1psubm  43160  deg1mhm  43161  isotone1  44010  isotone2  44011  mnringmulrcld  44197  traxext  44910  disjxp1  44971  disjf1  45090  wessf1ornlem  45092  projf1o  45104  sumnnodd  45551  lptioo2  45552  lptioo1  45553  cncfshift  45795  cncfperiod  45800  dvnprodlem1  45867  fourierdlem42  46070  nnfoctbdjlem  46376  isomennd  46452  smflimlem6  46697  fsetsnf1  46967  cfsetsnfsetf1  46974  otiunsndisjX  47194  imasetpreimafvbijlemf1  47278  iccpartgt  47301  icceuelpart  47310  ichnreuop  47346  sprsymrelfolem2  47367  sprsymrelf  47369  prproropf1o  47381  reupr  47396  reuopreuprim  47400  isuspgrim0lem  47755  uspgrimprop  47757  opmpoismgm  47890  mgmplusgiopALT  47917  2zlidl  47963  rhmsubcALTV  48008  srhmsubcALTV  48048  fldhmsubcALTV  48056  lindslinindsimp1  48186  1arymaptf1  48376  2arymaptf1  48387  toslat  48654  catprsc  48680  catprsc2  48681  isthincd  48704  isthincd2  48705  functhinclem4  48711  thincfth  48715  thincciso  48716