Theorem ralrimivva 2632

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  swopo  4451  sosng  4848  fcof1  5989  fliftfund  6003  isoresbr  6015  isocnv  6017  f1oiso  6032  oveqrspc2v  6112  caovclg  6242  caovcomg  6245  off  6315  caofrss  6334  caofdig  6336  oprssdmm  6405  dmmpog  6445  fnmpoovd  6451  fmpoco  6452  poxp  6468  f1od2  6471  suppofss1dcl  6504  suppofss2dcl  6505  eroprf  6902  dom2lem  7058  xpf1o  7144  fidifsnid  7173  nnwetri  7223  undiffi  7232  fidcenumlemim  7269  supmoti  7334  supsnti  7346  supisoti  7351  difinfsnlem  7440  nninfwlpor  7515  netap  7621  2omotaplemap  7624  cc2lem  7633  addlocpr  7904  mullocpr  7939  cauappcvgprlemloc  8020  cauappcvgprlemlim  8029  caucvgprlemloc  8043  caucvgprprlemloc  8071  suplocexprlemloc  8089  suplocsrlemb  8174  rereceu  8257  axpre-suploclemres  8269  ltordlem  8812  cju  9294  exbtwnz  10696  frec2uzf1od  10858  frec2uzisod  10859  frecuzrdgrrn  10860  frec2uzrdg  10861  frecuzrdgrcl  10862  frecuzrdgsuc  10866  frecuzrdgrclt  10867  frecuzrdgg  10868  frecuzrdgsuctlem  10875  seqvalcd  10913  seqovcd  10919  seq3caopr3  10943  seq3caopr2  10945  seqcaopr2g  10946  iseqf1olemqf1o  10958  seq3homo  10979  seqhomog  10982  seqfeq4g  10983  seq3distr  10984  fimaxq  11286  zfz1isolem1  11308  wrd2ind  11511  rsqrmo  11809  climcn2  12094  addcn2  12095  mulcn2  12097  fsum2dlemstep  12220  fisumcom2  12224  cvgratnn  12317  fprodcl2lem  12391  fprod2dlemstep  12408  fprodcom2fi  12412  divalglemeunn  12707  divalglemeuneg  12709  bezoutlemeu  12803  isprm6  12945  pwbdvdseu  12966  crth  13025  eulerthlemh  13032  4sqlemffi  13198  ennnfonelemim  13367  nninfdclemf1  13395  unbendc  13397  imasaddfnlemg  13688  ercpbl  13705  plusffng  13738  mgmplusf  13739  opifismgmdc  13744  issgrpd  13780  sgrppropd  13781  ismndd  13803  mndpropd  13806  issubmnd  13808  mndinvmod  13811  mhmpropd  13826  idmhm  13829  mhmf1o  13830  issubmd  13834  mndissubm  13835  submid  13837  0mhm  13846  resmhm  13847  resmhm2  13848  resmhm2b  13849  mhmco  13850  grppropd  13875  grpsubf  13937  dfgrp3m  13957  mhmmnd  13972  mhmfmhm  13973  mulgfng  13980  issubg4m  14049  grpissubg  14050  isnsg3  14063  0nsg  14070  nsgid  14071  isghmd  14108  ghmmhm  14109  idghm  14115  ghmnsgima  14124  ghmnsgpreima  14125  ghmf1  14129  kerf1ghm  14130  ghmf1o  14131  cntzsgrpcl  14161  cntzsubm  14164  cntrsubgnsg  14169  cmnsubm  14196  ghmcmn  14215  invghm  14217  ablnsg  14222  imasabl  14224  srgfcl  14361  srglmhm  14381  srgrmhm  14382  isrhm2d  14556  subrngringnsg  14597  issubrng2  14602  subrngintm  14604  issubrg2  14633  subrgintm  14635  aprap  14682  aprlring  14684  islmodd  14713  lmodscaf  14731  lmodprop2d  14769  islssmd  14780  islss4  14803  lsspropdg  14852  issubrgd  14873  dflidl2rng  14902  rnglidlmmgm  14917  expghmap  15026  mulgghm2  15027  znf1o  15070  znidom  15076  issubassa2  15119  tgclb  15257  txbas  15450  txcnp  15463  txcnmpt  15465  cnmpt21  15483  txswaphmeo  15513  isxmetd  15539  isxmet2d  15540  xmettpos  15562  blfvalps  15577  xmetresbl  15632  metss2  15690  comet  15691  bdmet  15694  bdmopn  15696  xmetxp  15699  qtopbasss  15713  elcncf1di  15771  cncfcdm  15774  mulc1cncf  15781  cncfco  15783  dedekindeulemloc  15811  dedekindeu  15815  dedekindicclemloc  15820  dedekindicclemicc  15824  ivthinclemloc  15833  dich0  15844  dvmptfsum  15917  mpodvdsmulf1o  16245  fsumdvdsmul  16246  gausslemma2dlem1f1o  16345  lgseisenlem2  16356  lgsquadlemsfi  16360  lgsquadlem1  16362  lgsquadlem2  16363  lgsquadlem3  16364  usgredgreu  16623  uspgredg2vtxeu  16625  uspgredg2v  16628  usgredg2v  16631  vtxedgfi  16696  vtxlpfi  16697  dichmul0or  16926  sssneq  17198  exmidsbthrlem  17233  cvgcmp2n  17248  trirec0  17260  apdiff  17264  redc0  17274  reap0  17275  cndcap  17276  neap0mkv  17286