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  10511  frec2uzf1od  10669  frec2uzisod  10670  frecuzrdgrrn  10671  frec2uzrdg  10672  frecuzrdgrcl  10673  frecuzrdgsuc  10677  frecuzrdgrclt  10678  frecuzrdgg  10679  frecuzrdgsuctlem  10686  seqvalcd  10724  seqovcd  10730  seq3caopr3  10754  seq3caopr2  10756  seqcaopr2g  10757  iseqf1olemqf1o  10769  seq3homo  10790  seqhomog  10793  seqfeq4g  10794  seq3distr  10795  fimaxq  11092  zfz1isolem1  11105  wrd2ind  11308  rsqrmo  11605  climcn2  11887  addcn2  11888  mulcn2  11890  fsum2dlemstep  12013  fisumcom2  12017  cvgratnn  12110  fprodcl2lem  12184  fprod2dlemstep  12201  fprodcom2fi  12205  divalglemeunn  12500  divalglemeuneg  12502  bezoutlemeu  12596  isprm6  12737  pw2dvdseu  12758  crth  12814  eulerthlemh  12821  4sqlemffi  12987  ennnfonelemim  13063  nninfdclemf1  13091  unbendc  13093  imasaddfnlemg  13415  ercpbl  13432  plusffng  13466  mgmplusf  13467  opifismgmdc  13472  issgrpd  13513  sgrppropd  13514  ismndd  13538  mndpropd  13541  issubmnd  13543  mndinvmod  13546  mhmpropd  13567  idmhm  13570  mhmf1o  13571  issubmd  13575  mndissubm  13576  submid  13578  0mhm  13587  resmhm  13588  resmhm2  13589  resmhm2b  13590  mhmco  13591  grppropd  13618  grpsubf  13680  dfgrp3m  13700  mhmmnd  13721  mhmfmhm  13722  mulgfng  13729  issubg4m  13798  grpissubg  13799  isnsg3  13812  0nsg  13819  nsgid  13820  isghmd  13857  ghmmhm  13858  idghm  13864  ghmnsgima  13873  ghmnsgpreima  13874  ghmf1  13878  kerf1ghm  13879  ghmf1o  13880  ghmcmn  13932  invghm  13934  ablnsg  13939  imasabl  13941  srgfcl  14005  srglmhm  14025  srgrmhm  14026  isrhm2d  14198  subrngringnsg  14238  issubrng2  14243  subrngintm  14245  issubrg2  14274  subrgintm  14276  aprap  14319  islmodd  14326  lmodscaf  14343  lmodprop2d  14381  islssmd  14392  islss4  14415  lsspropdg  14464  issubrgd  14485  dflidl2rng  14514  rnglidlmmgm  14529  expghmap  14640  mulgghm2  14641  znf1o  14684  znidom  14690  tgclb  14808  txbas  15001  txcnp  15014  txcnmpt  15016  cnmpt21  15034  txswaphmeo  15064  isxmetd  15090  isxmet2d  15091  xmettpos  15113  blfvalps  15128  xmetresbl  15183  metss2  15241  comet  15242  bdmet  15245  bdmopn  15247  xmetxp  15250  qtopbasss  15264  elcncf1di  15322  cncfcdm  15325  mulc1cncf  15332  cncfco  15334  dedekindeulemloc  15362  dedekindeu  15366  dedekindicclemloc  15371  dedekindicclemicc  15375  ivthinclemloc  15384  dich0  15395  dvmptfsum  15468  mpodvdsmulf1o  15733  fsumdvdsmul  15734  gausslemma2dlem1f1o  15808  lgseisenlem2  15819  lgsquadlemsfi  15823  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  usgredgreu  16086  uspgredg2vtxeu  16088  uspgredg2v  16091  usgredg2v  16094  vtxedgfi  16159  vtxlpfi  16160  sssneq  16654  exmidsbthrlem  16677  cvgcmp2n  16688  trirec0  16699  apdiff  16703  redc0  16713  reap0  16714  cndcap  16715  neap0mkv  16725