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  4453  sosng  4850  fcof1  5992  fliftfund  6006  isoresbr  6018  isocnv  6020  f1oiso  6035  oveqrspc2v  6115  caovclg  6245  caovcomg  6248  off  6319  caofrss  6338  caofdig  6340  oprssdmm  6409  dmmpog  6449  fnmpoovd  6455  fmpoco  6456  poxp  6472  f1od2  6475  suppofss1dcl  6508  suppofss2dcl  6509  eroprf  6907  dom2lem  7064  xpf1o  7150  fidifsnid  7179  nnwetri  7229  undiffi  7238  fidcenumlemim  7276  supmoti  7339  supsnti  7351  supisoti  7356  difinfsnlem  7445  nninfwlpor  7520  netap  7626  2omotaplemap  7629  cc2lem  7638  addlocpr  7909  mullocpr  7944  cauappcvgprlemloc  8025  cauappcvgprlemlim  8034  caucvgprlemloc  8048  caucvgprprlemloc  8076  suplocexprlemloc  8094  suplocsrlemb  8179  rereceu  8262  axpre-suploclemres  8274  ltordlem  8817  cju  9299  fcdmnn0fsuppfi  9743  exbtwnz  10701  frec2uzf1od  10863  frec2uzisod  10864  frecuzrdgrrn  10865  frec2uzrdg  10866  frecuzrdgrcl  10867  frecuzrdgsuc  10871  frecuzrdgrclt  10872  frecuzrdgg  10873  frecuzrdgsuctlem  10880  seqvalcd  10918  seqovcd  10924  seq3caopr3  10948  seq3caopr2  10950  seqcaopr2g  10951  iseqf1olemqf1o  10963  seq3homo  10984  seqhomog  10987  seqfeq4g  10988  seq3distr  10989  fimaxq  11291  zfz1isolem1  11313  wrd2ind  11516  rsqrmo  11814  climcn2  12099  addcn2  12100  mulcn2  12102  fsum2dlemstep  12225  fisumcom2  12229  cvgratnn  12322  fprodcl2lem  12396  fprod2dlemstep  12413  fprodcom2fi  12417  divalglemeunn  12712  divalglemeuneg  12714  bezoutlemeu  12808  isprm6  12950  pwbdvdseu  12971  crth  13030  eulerthlemh  13037  4sqlemffi  13203  ennnfonelemim  13372  nninfdclemf1  13400  unbendc  13402  imasaddfnlemg  13693  ercpbl  13710  plusffng  13743  mgmplusf  13744  opifismgmdc  13749  issgrpd  13785  sgrppropd  13786  ismndd  13808  mndpropd  13811  issubmnd  13813  mndinvmod  13816  mhmpropd  13831  idmhm  13834  mhmf1o  13835  issubmd  13839  mndissubm  13840  submid  13842  0mhm  13851  resmhm  13852  resmhm2  13853  resmhm2b  13854  mhmco  13855  grppropd  13880  grpsubf  13942  dfgrp3m  13962  mhmmnd  13977  mhmfmhm  13978  mulgfng  13985  issubg4m  14054  grpissubg  14055  isnsg3  14068  0nsg  14075  nsgid  14076  isghmd  14113  ghmmhm  14114  idghm  14120  ghmnsgima  14129  ghmnsgpreima  14130  ghmf1  14134  kerf1ghm  14135  ghmf1o  14136  cntzsgrpcl  14166  cntzsubm  14169  cntrsubgnsg  14174  cmnsubm  14201  ghmcmn  14220  invghm  14222  ablnsg  14227  imasabl  14229  gsum2d2fi  14273  gsumcom2fi  14274  srgfcl  14383  srglmhm  14403  srgrmhm  14404  isrhm2d  14580  subrngringnsg  14621  issubrng2  14626  subrngintm  14628  issubrg2  14657  subrgintm  14659  aprap  14706  aprlring  14708  islmodd  14737  lmodscaf  14755  lmodprop2d  14793  islssmd  14804  islss4  14827  lsspropdg  14876  issubrgd  14897  dflidl2rng  14926  rnglidlmmgm  14941  expghmap  15050  mulgghm2  15051  znf1o  15094  znidom  15100  issubassa2  15143  mvrf1fi  15219  tgclb  15308  txbas  15501  txcnp  15514  txcnmpt  15516  cnmpt21  15534  txswaphmeo  15564  isxmetd  15590  isxmet2d  15591  xmettpos  15613  blfvalps  15628  xmetresbl  15683  metss2  15741  comet  15742  bdmet  15745  bdmopn  15747  xmetxp  15750  qtopbasss  15764  elcncf1di  15822  cncfcdm  15825  mulc1cncf  15832  cncfco  15834  dedekindeulemloc  15862  dedekindeu  15866  dedekindicclemloc  15871  dedekindicclemicc  15875  ivthinclemloc  15884  dich0  15895  dvmptfsum  15968  mpodvdsmulf1o  16301  fsumdvdsmul  16302  gausslemma2dlem1f1o  16401  lgseisenlem2  16412  lgsquadlemsfi  16416  lgsquadlem1  16418  lgsquadlem2  16419  lgsquadlem3  16420  usgredgreu  16679  uspgredg2vtxeu  16681  uspgredg2v  16684  usgredg2v  16687  vtxedgfi  16752  vtxlpfi  16753  dichmul0or  16982  sssneq  17254  exmidsbthrlem  17290  cvgcmp2n  17305  trirec0  17317  apdiff  17321  redc0  17331  reap0  17332  cndcap  17333  neap0mkv  17343