Theorem ralrimivva 3207

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3079

This theorem is used by:  disjord  5096  disjxiun  5104  otsndisj  5500  otiunsndisj  5501  swopo  5578  issod  5602  reuop  6295  fcof1  7291  fliftfund  7317  isof1oidb  7328  isof1oopb  7329  soisores  7331  soisoi  7332  isocnv  7334  f1oiso  7355  oveqrspc2v  7443  oprres  7584  caovclg  7609  caovcomg  7612  off  7699  coof  7705  caofidlcan  7719  caofrss  7720  caonncan  7725  fmpodg  8072  dmmpog  8076  fnmpoovd  8087  fmpoco  8095  fsplitfpar  8118  poxp  8129  fvmpocurryd  8272  smo11  8356  smoiso2  8361  omsmo  8649  nnasmo  8654  coflton  8662  qsdisj2  8798  eroprf  8818  uncf  8873  dom2lem  9001  omxpenlem  9079  xpf1o  9140  unxpdomlem3  9231  fofinf1o  9302  dffi3  9404  supmo  9425  infmo  9470  inf3lem6  9615  cantnf  9675  rankxplim  9864  fseqenlem1  10030  fodomacn  10062  iunfictbso  10120  cofsmo  10274  infpssrlem5  10312  enfin2i  10326  fin23lem23  10331  fin23lem27  10333  fin23lem28  10345  compssiso  10379  ltordlem  11766  cju  12241  axdc4uzlem  14049  seqcaopr2  14104  seqhomo  14115  ccatf1  14658  swrdf1  14721  wrd2ind  14794  cshf1  14883  s3sndisj  15042  s3iunsndisj  15043  climcn2  15682  addcn2  15683  mulcn2  15685  o1of2  15702  isercolllem1  15754  fsum2dlem  15858  fsumcom2  15862  fprodser  16040  fprod2dlem  16071  fprodcom2  16075  isprm6  16809  crth  16873  eulerthlem2  16877  vdwlem12  17088  cshwsdisj  17194  imasaddfnlem  17618  imasvscafn  17627  mreexexd  17740  iscatd  17765  oppccomfpropd  17819  isofn  17868  sectmon  17875  ssctr  17918  ssceq  17919  catsubcat  17932  issubc3  17942  fullsubc  17943  fullresc  17944  isfuncd  17958  idfucl  17974  cofucl  17981  funcres2b  17990  fulloppc  18017  fthoppc  18018  idffth  18028  cofull  18029  cofth  18030  ressffth  18033  setcmon  18180  setcepi  18181  resssetc  18185  resscatc  18202  catciso  18204  fthestrcsetc  18242  fullestrcsetc  18243  embedsetcestrclem  18249  fthsetcestrc  18257  fullsetcestrc  18258  evlfcl  18314  uncfcurf  18331  hofcl  18351  yonedalem3  18372  yonedainv  18373  yonffthlem  18374  yoniso  18377  isdrs2  18398  isposd  18414  pospropd  18417  poslubmo  18501  posglbmo  18502  chnpof1  18722  mgmplusf  18744  mgmn0plusgf  18745  ismgmd  18748  issstrmgm  18749  opifismgm  18755  mgmhmpropd  18802  mgmhmf1o  18804  idmgmhm  18805  issubmgm2  18807  rabsubmgmd  18808  resmgmhm  18815  resmgmhm2  18816  resmgmhm2b  18817  mgmhmco  18818  submgmacs  18821  issgrpd  18834  sgrppropd  18835  ismndd  18861  mndpropd  18866  issubmnd  18868  mndinvmod  18873  ismhmd  18895  mhmpropd  18901  idmhm  18904  mhmf1o  18905  issubmd  18915  mndissubm  18916  0mhm  18929  resmhm  18930  resmhm2  18931  resmhm2b  18932  mhmco  18933  submacs  18937  prdspjmhm  18939  pwsdiagmhm  18941  pwsco1mhm  18942  pwsco2mhm  18943  gsumwspan  18956  frmdsssubm  18971  frmdup1  18974  grpsubf  19143  dfgrp3  19163  mhmmnd  19188  mhmfmhm  19189  issubg4  19270  grpissubg  19271  isnsg3  19284  nsgacs  19286  0nsg  19293  nsgid  19294  qus0subgadd  19328  cycsubmcom  19333  isghmd  19353  ghmmhm  19354  idghm  19359  ghmnsgima  19368  ghmnsgpreima  19369  ghmf1  19374  kerf1ghm  19375  ghmf1o  19376  gaid  19427  subgga  19428  gass  19429  gasubg  19430  cntzsgrpcl  19462  cntzsubm  19466  cntrsubgnsg  19471  lactghmga  19533  symgfixf1  19565  odf1  19690  sylow1lem2  19727  sylow2blem2  19749  sylow3lem1  19755  lsmssv  19771  smndlsmidm  19784  pj1eu  19824  efglem  19844  efgtf  19850  efgred  19876  efgredeu  19880  frgpmhm  19893  frgpuptf  19898  frgpuplem  19900  mulgmhm  19955  ghmcmn  19959  invghm  19961  ablnsg  19975  imasabl  20004  cygabl  20019  gsum2d2lem  20101  gsum2d2  20102  gsumcom2  20103  dprd2d2  20174  ablfaclem2  20216  srgfcl  20336  srgcom4lem  20353  srglmhm  20361  srgrmhm  20362  ringcomlem  20421  isrnghm2d  20592  c0mgm  20601  c0mhm  20602  isrhm2d  20633  subrngringnsg  20716  issubrng2  20721  subrngint  20723  issubrg2  20755  subrgint  20758  rnghmsscmap2  20792  rnghmsscmap  20793  rnghmsubcsetclem2  20795  rhmsscmap2  20821  rhmsscmap  20822  rhmsubcsetclem2  20824  rhmsscrnghm  20828  rhmsubcrngclem2  20830  srhmsubc  20843  rhmsubc  20852  fldhmsubc  20952  primefld  20972  abvn0b  21003  suborng  21043  islmodd  21051  lmodscaf  21069  lmodprop2d  21109  islssd  21120  islss4  21147  lssacs  21152  lsspropd  21202  islmhmd  21224  lmhmima  21232  lmhmpreima  21233  reslmhm  21237  lspextmo  21241  lsmcl  21268  pj1lmhm  21285  islbs2  21342  issubrgd  21374  dflidl2rng  21407  rnglidlmmgm  21443  rhmpreimaidl  21480  rngqiprnglin  21506  prmidl2  21530  idlmulssprm  21531  isprmidlc  21536  rhmpreimaprmidl  21543  qsidomlem1  21544  qsidomlem2  21545  ssdifidllem  21548  ssdifidlprm  21550  prmidlsubm  21551  expmhm  21650  nn0srg  21651  prmirredlem  21686  expghm  21689  mulgghm2  21690  domnchr  21746  znf1o  21765  zntoslem  21770  znfld  21774  cygznlem3  21783  phlipf  21866  dsmmlss  21958  uvcf1  22006  frlmlbs  22011  lindff1  22034  lindfrn  22035  f1lindf  22036  issubassa2  22108  mvrf1  22201  mplsubglem  22214  mplsubrg  22220  mplcoe5lem  22256  mplcoe2  22258  mplind  22287  evlslem2  22296  evlseu  22300  mhplss  22384  ply1sclf1  22516  evls1maplmhm  22603  mamucl  22624  mamuass  22625  mamudi  22626  mamudir  22627  mamuvs1  22628  mamuvs2  22629  matbas2d  22646  mamumat1cl  22662  mamulid  22664  mamurid  22665  mat1mhm  22707  dmatid  22718  dmatsubcl  22721  dmatsgrp  22722  dmatmulcl  22723  dmatsrng  22724  dmatcrng  22725  scmatscmiddistr  22731  scmatscm  22736  scmatsgrp  22742  scmatsrng  22743  scmatcrng  22744  scmatsgrp1  22745  scmatsrng1  22746  scmatf1  22754  scmatmhm  22757  mavmul0g  22776  mdet1  22824  mdetunilem9  22843  mdetuni0  22844  mdetmul  22846  madutpos  22865  smadiadetlem4  22892  1elcpmat  22941  cpmatacl  22942  cpmatmcl  22945  mat2pmatf1  22955  mat2pmatmul  22957  mat2pmat1  22958  mat2pmatlin  22961  m2cpm  22967  m2cpminvid  22979  m2cpminvid2  22981  decpmatmul  22998  pmatcollpw1  23002  monmatcollpw  23005  pmatcollpw  23007  pmatcollpw3lem  23009  pmatcollpwscmatlem2  23016  pm2mpf1  23025  mp2pm2mplem4  23035  pm2mpmhmlem2  23045  chp0mat  23072  chpidmat  23073  tgclb  23196  mretopd  23318  toponmre  23319  iscldtop  23321  ordtbaslem  23414  ordtbas2  23417  cnt0  23572  haust1  23578  cnhaus  23580  isreg2  23603  dishaus  23608  ordthaus  23610  dfconn2  23645  iunconn  23654  clsconn  23656  2ndcomap  23685  dis2ndc  23687  llynlly  23704  restnlly  23709  restlly  23710  islly2  23711  llyidm  23715  nllyidm  23716  hausllycmp  23721  kgentopon  23765  txbas  23794  ptbasin2  23805  ptbasfi  23808  txcnp  23847  txcnmpt  23851  pthaus  23865  tx1stc  23877  xkococnlem  23886  xkococn  23887  cnmpt21  23898  qtoptop2  23926  qtopeu  23943  kqt0lem  23963  isr0  23964  regr1lem2  23967  kqreglem1  23968  kqreglem2  23969  kqnrmlem1  23970  kqnrmlem2  23971  nrmr0reg  23976  reghmph  24020  nrmhmph  24021  txswaphmeo  24032  qtophmeo  24044  fbun  24067  trfbas2  24070  isfil2  24083  infil  24090  trfil2  24114  filssufilg  24138  hausflim  24208  fclsnei  24246  fclsfnflim  24254  flimfnfcls  24255  ptcmplem1  24279  clssubg  24336  tgpconncomp  24340  qustgplem  24348  tsmsfbas  24355  utoptop  24461  iducn  24509  cstucnd  24510  isxmetd  24553  isxmet2d  24554  xmettpos  24576  prdsdsf  24594  prdsmet  24597  ressprdsds  24598  imasdsf1olem  24600  imasf1oxmet  24602  imasf1omet  24603  blfvalps  24610  xmetresbl  24664  metss2  24739  comet  24740  stdbdmet  24743  stdbdmopn  24745  methaus  24747  met2ndci  24749  metustfbas  24784  nrmmetd  24801  subgngp  24862  ngptgp  24863  sranlm  24911  nlmvscnlem1  24913  nlmvscn  24914  nrginvrcn  24919  lssnlm  24928  nghmcn  24972  qtopbaslem  24985  reconn  25056  xmetdcn2  25065  metdscn  25084  metnrm  25090  elcncf1di  25124  cncfcdm  25127  mulc1cncf  25134  cncfco  25136  reparphti  25226  isncvsngpd  25379  tcphcph  25466  ipcnlem1  25474  ipcn  25475  iscfil3  25502  bcthlem5  25557  rrxmet  25637  minveclem3  25658  minveclem7  25664  ovolicc2lem4  25749  dyadmbl  25829  volcn  25835  itg1addlem1  25921  itg1addlem2  25926  itg1addlem4  25928  mbfi1fseqlem1  25944  mbfi1fseqlem3  25946  mbfi1fseqlem4  25947  mbfi1fseqlem5  25948  dvmptfsum  26204  c1liplem1  26225  dvgt0lem2  26232  ftc1a  26266  ply1domn  26351  ply1divmo  26363  fta1b  26399  ig1peu  26402  coeeu  26452  plydivalg  26530  aaliou2b  26574  ulmss  26630  ulmcn  26632  efif1olem4  26780  efsubm  26786  logccv  26898  logbmpt  27023  logbfval  27025  cvxcl  27219  basellem4  27318  fsumdvdscom  27419  musum  27425  mpodvdsmulf1o  27428  fsumdvdsmul  27429  dvdsmulf1o  27430  dchrelbasd  27473  dchrmulcl  27483  dchrinv  27495  lgsqrlem2  27581  lgsdchr  27589  lgseisenlem2  27610  lgsquadlem1  27614  lgsquadlem2  27615  2sqreulem4  27688  dchrisumlema  27722  dchrisumlem2  27724  chpdifbndlem2  27788  pntpbnd  27822  pntibndlem3  27826  sltsd  28031  oldbday  28164  addsprop  28239  mulcutlem  28394  divsmo  28447  om2noseqf1o  28564  om2noseqiso  28565  axtgcont  28808  tgjustc1  28814  tgjustc2  28815  tgsegconeu  28826  iscgrglt  28854  ercgrg  28857  idmot  28877  motco  28880  cnvmot  28881  motcgrg  28884  tgisline  28972  tghilberti2  28983  mirreu3  29003  mirmot  29024  ragperp  29069  foot  29074  mideu  29091  midf  29158  lmimot  29180  trgcopyeu  29190  prlngmolem1  29295  f1otrgds  29311  f1otrg  29313  f1otrge  29314  xmstrkgc  29328  brbtwn2  29348  axlowdimlem15  29399  axcontlem2  29408  axcontlem10  29416  eengtrkg  29429  eengtrkge  29430  numedglnl  29587  usgredgreu  29664  uspgredg2vtxeu  29666  uspgredg2v  29670  usgredg2v  29673  wlkswwlksf1o  30333  wwlksnextinj  30353  clwlkclwwlkf1  30466  clwwlkf1  30505  frcond4  30736  frgrncvvdeqlem8  30772  frgrncvvdeq  30775  frgrwopreglem4  30781  numclwwlk1lem2f1  30823  nrt2irr  30939  grpoinvf  30999  nvmf  31112  vacn  31161  nmcvcn  31162  smcnlem  31164  sspg  31195  ssps  31197  sspmlem  31199  0lno  31257  blocni  31272  ipblnfi  31322  minvecolem7  31350  unopf1o  32383  cnvunop  32385  unoplin  32387  counop  32388  hmopadj2  32408  hmoplin  32409  bralnfn  32415  lnopeq0i  32474  hmops  32487  hmopm  32488  hmopco  32490  lnconi  32500  cnlnadjlem2  32535  adjmul  32559  adjadd  32560  cdjreui  32899  disjxpin  33048  off2  33101  2ndresdju  33109  fnpreimac  33130  suppovss  33140  f1od2  33177  xrofsup  33225  s3f1  33377  odutos  33395  dfmgc2lem  33422  dfmgc2  33423  pwrssmgc  33427  mgcf1o  33430  mndlactf1  33453  mndractf1  33455  abliso  33462  symgcntz  33512  tocyccntz  33571  conjga  33597  fxpsubrg  33601  archiabllem1  33620  archiabllem2  33624  urpropd  33657  elrgspnlem2  33670  rlocf1  33701  rrgsubm  33711  subrdom  33712  ricdomn1  33716  xrge0slmod  33775  nsgmgc  33828  intlidl  33835  idlinsubrg  33846  rhmimaidl  33847  mxidlprm  33860  mxidlirredi  33861  ssmxidllem  33863  drnglring  33889  dflringlem2  33892  rsprprmprmidl  33919  rsprprmprmidlb  33920  rprmirred  33928  rprmirredb  33929  1arithufdlem4  33944  selvply1rhmlema  34015  selvply1rhmlem1  34017  mplidomlem  34024  extvfvcl  34033  mplvrpmga  34042  ply1degltdimlem  34119  ply1degltdim  34120  lindsun  34122  fedgmullem1  34126  fedgmullem2  34127  fedgmul  34128  lactlmhm  34131  assalactf1o  34132  minplyirred  34208  constrsdrg  34272  1smat1  34301  submateq  34306  madjusmdetlem3  34326  zart0  34376  pstmxmet  34394  ofcf  34600  ldgenpisys  34664  rossros  34678  inelcarsg  34809  sibfof  34838  sitmf  34850  hgt750lemb  35151  erdszelem4  35760  erdszelem9  35765  erdsze2lem2  35770  cnpconn  35796  pconnconn  35797  txpconn  35798  ptpconn  35799  cvxpconn  35808  cvxsconn  35809  iccllysconn  35816  cvmseu  35842  cvmliftmo  35850  cvmlift2lem5  35873  cvmlift2lem9  35877  mrsubff1  36080  elmrsubrn  36086  mrsubco  36087  msubff1  36122  mvhf1  36125  r1peuqusdeg1  36209  segconeu  36578  nmulprop  36757  nadddilem4  36790  fnessref  36963  neibastop1  36965  filnetlem3  36986  onsuct0  37047  weiunlem  37069  mh-inf3f1  37147  unblimceq0lem  37190  unbdqndv2  37195  knoppndv  37218  irrdiff  38065  fin2so  38348  lindsadd  38354  poimirlem4  38360  poimirlem13  38369  poimirlem14  38370  poimirlem26  38382  heicant  38391  mblfinlem2  38394  ftc1anc  38437  sdclem1  38480  isbnd3  38521  prdsbnd  38530  ismtycnv  38539  ismtyhmeolem  38541  ismtyres  38545  bfplem1  38559  bfplem2  38560  bfp  38561  rrnmet  38566  ismrer1  38575  iccbnd  38577  grpokerinj  38630  isdrngo2  38695  rngogrphom  38708  rngohomco  38711  rngoisocnv  38718  iscringd  38735  eqvreldisj1  39662  erprt  39733  lfl0f  39929  lkrlss  39955  lshpsmreu  39969  linepsubN  40612  pmapsub  40628  lautcnv  40950  lautco  40957  idltrn  41010  cdleme50f1  41403  cdleme50laut  41407  istendod  41622  dihf11  42127  dih1dimatlem  42189  lcfl7N  42361  lcfrlem9  42410  mapd1o  42508  hdmapf1oN  42725  hgmapf1oN  42763  fmpocos  43090  qsalrel  43095  rediveud  43305  imacrhmcl  43389  evlselv  43422  fsuppind  43423  nacsfix  43544  rmxypairf1o  43739  wepwsolem  43870  dnnumch3  43875  fnwe2  43881  mpaaeu  43978  idomsubgmo  44021  mon1psubm  44027  deg1mhm  44028  isotone1  44875  isotone2  44876  mnringmulrcld  45053  traxext  45787  disjxp1  45890  disjf1  46002  wessf1ornlem  46004  projf1o  46015  sumnnodd  46447  lptioo2  46448  lptioo1  46449  cncfshift  46689  cncfperiod  46694  dvnprodlem1  46761  fourierdlem42  46964  nnfoctbdjlem  47270  isomennd  47346  smflimlem6  47591  fsetsnf1  47927  cfsetsnfsetf1  47934  otiunsndisjX  48154  imasetpreimafvbijlemf1  48291  iccpartgt  48314  icceuelpart  48323  ichnreuop  48359  sprsymrelfolem2  48380  sprsymrelf  48382  prproropf1o  48394  reupr  48409  reuopreuprim  48413  uhgrimprop  48795  isuspgrim0lem  48796  upgrimtrls  48809  gpgprismgr4cycllem11  49008  opmpoismgm  49069  mgmplusgiopALT  49096  2zlidl  49142  rhmsubcALTV  49187  srhmsubcALTV  49227  fldhmsubcALTV  49235  lindslinindsimp1  49374  1arymaptf1  49559  2arymaptf1  49570  eqfnovd  49781  toslat  49895  catprsc  49926  catprsc2  49927  oppcendc  49931  invfn  49943  iinfssclem2  49968  iinfssc  49970  iinfsubc  49971  discsubc  49977  nelsubclem  49980  resccatlem  49986  funchomf  50010  imasubclem2  50018  imaidfu  50023  imasubc  50064  imassc  50066  imasubc3  50069  fthcomf  50070  idfth  50071  cofidfth  50075  upeu2  50085  isnatd  50136  swapfffth  50196  diag1f1  50220  diag2f1  50222  fucoppc  50323  isthincd  50349  isthincd2  50350  oppcthinco  50352  oppcthinendcALT  50354  functhinclem4  50360  functhincfun  50362  thincfth  50365  thincciso  50366  thinccisod  50367  functermc  50421  arweuthinc  50442  arweutermc  50443  diagffth  50451  funcsn  50454  0fucterm  50456  veronesematrowd  50801  veroquadmodzerod  50804