Theorem ralrimivva 2614

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  ∀wral 2510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-4 1558  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  swopo  4403  sosng  4799  fcof1  5924  fliftfund  5938  isoresbr  5950  isocnv  5952  f1oiso  5967  oveqrspc2v  6045  caovclg  6175  caovcomg  6178  off  6248  caofrss  6267  caofdig  6269  oprssdmm  6334  dmmpog  6374  fnmpoovd  6380  fmpoco  6381  poxp  6397  f1od2  6400  eroprf  6797  dom2lem  6945  xpf1o  7030  fidifsnid  7058  nnwetri  7108  undiffi  7117  fidcenumlemim  7151  supmoti  7192  supsnti  7204  supisoti  7209  difinfsnlem  7298  nninfwlpor  7373  netap  7473  2omotaplemap  7476  cc2lem  7485  addlocpr  7756  mullocpr  7791  cauappcvgprlemloc  7872  cauappcvgprlemlim  7881  caucvgprlemloc  7895  caucvgprprlemloc  7923  suplocexprlemloc  7941  suplocsrlemb  8026  rereceu  8109  axpre-suploclemres  8121  ltordlem  8662  cju  9141  exbtwnz  10510  frec2uzf1od  10668  frec2uzisod  10669  frecuzrdgrrn  10670  frec2uzrdg  10671  frecuzrdgrcl  10672  frecuzrdgsuc  10676  frecuzrdgrclt  10677  frecuzrdgg  10678  frecuzrdgsuctlem  10685  seqvalcd  10723  seqovcd  10729  seq3caopr3  10753  seq3caopr2  10755  seqcaopr2g  10756  iseqf1olemqf1o  10768  seq3homo  10789  seqhomog  10792  seqfeq4g  10793  seq3distr  10794  fimaxq  11091  zfz1isolem1  11104  wrd2ind  11304  rsqrmo  11588  climcn2  11870  addcn2  11871  mulcn2  11873  fsum2dlemstep  11996  fisumcom2  12000  cvgratnn  12093  fprodcl2lem  12167  fprod2dlemstep  12184  fprodcom2fi  12188  divalglemeunn  12483  divalglemeuneg  12485  bezoutlemeu  12579  isprm6  12720  pw2dvdseu  12741  crth  12797  eulerthlemh  12804  4sqlemffi  12970  ennnfonelemim  13046  nninfdclemf1  13074  unbendc  13076  imasaddfnlemg  13398  ercpbl  13415  plusffng  13449  mgmplusf  13450  opifismgmdc  13455  issgrpd  13496  sgrppropd  13497  ismndd  13521  mndpropd  13524  issubmnd  13526  mndinvmod  13529  mhmpropd  13550  idmhm  13553  mhmf1o  13554  issubmd  13558  mndissubm  13559  submid  13561  0mhm  13570  resmhm  13571  resmhm2  13572  resmhm2b  13573  mhmco  13574  grppropd  13601  grpsubf  13663  dfgrp3m  13683  mhmmnd  13704  mhmfmhm  13705  mulgfng  13712  issubg4m  13781  grpissubg  13782  isnsg3  13795  0nsg  13802  nsgid  13803  isghmd  13840  ghmmhm  13841  idghm  13847  ghmnsgima  13856  ghmnsgpreima  13857  ghmf1  13861  kerf1ghm  13862  ghmf1o  13863  ghmcmn  13915  invghm  13917  ablnsg  13922  imasabl  13924  srgfcl  13988  srglmhm  14008  srgrmhm  14009  isrhm2d  14181  subrngringnsg  14221  issubrng2  14226  subrngintm  14228  issubrg2  14257  subrgintm  14259  aprap  14302  islmodd  14309  lmodscaf  14326  lmodprop2d  14364  islssmd  14375  islss4  14398  lsspropdg  14447  issubrgd  14468  dflidl2rng  14497  rnglidlmmgm  14512  expghmap  14623  mulgghm2  14624  znf1o  14667  znidom  14673  tgclb  14791  txbas  14984  txcnp  14997  txcnmpt  14999  cnmpt21  15017  txswaphmeo  15047  isxmetd  15073  isxmet2d  15074  xmettpos  15096  blfvalps  15111  xmetresbl  15166  metss2  15224  comet  15225  bdmet  15228  bdmopn  15230  xmetxp  15233  qtopbasss  15247  elcncf1di  15305  cncfcdm  15308  mulc1cncf  15315  cncfco  15317  dedekindeulemloc  15345  dedekindeu  15349  dedekindicclemloc  15354  dedekindicclemicc  15358  ivthinclemloc  15367  dich0  15378  dvmptfsum  15451  mpodvdsmulf1o  15716  fsumdvdsmul  15717  gausslemma2dlem1f1o  15791  lgseisenlem2  15802  lgsquadlemsfi  15806  lgsquadlem1  15808  lgsquadlem2  15809  lgsquadlem3  15810  usgredgreu  16069  uspgredg2vtxeu  16071  uspgredg2v  16074  usgredg2v  16077  vtxedgfi  16142  vtxlpfi  16143  sssneq  16606  exmidsbthrlem  16629  cvgcmp2n  16640  trirec0  16651  apdiff  16655  redc0  16664  reap0  16665  cndcap  16666  neap0mkv  16676