Theorem ralrimivva 2612

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ∀wral 2508

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  swopo  4397  sosng  4792  fcof1  5907  fliftfund  5921  isoresbr  5933  isocnv  5935  f1oiso  5950  oveqrspc2v  6028  caovclg  6158  caovcomg  6161  off  6231  caofrss  6250  caofdig  6252  oprssdmm  6317  dmmpog  6355  fnmpoovd  6361  fmpoco  6362  poxp  6378  f1od2  6381  eroprf  6775  dom2lem  6923  xpf1o  7005  fidifsnid  7033  nnwetri  7078  undiffi  7087  fidcenumlemim  7119  supmoti  7160  supsnti  7172  supisoti  7177  difinfsnlem  7266  nninfwlpor  7341  netap  7440  2omotaplemap  7443  cc2lem  7452  addlocpr  7723  mullocpr  7758  cauappcvgprlemloc  7839  cauappcvgprlemlim  7848  caucvgprlemloc  7862  caucvgprprlemloc  7890  suplocexprlemloc  7908  suplocsrlemb  7993  rereceu  8076  axpre-suploclemres  8088  ltordlem  8629  cju  9108  exbtwnz  10470  frec2uzf1od  10628  frec2uzisod  10629  frecuzrdgrrn  10630  frec2uzrdg  10631  frecuzrdgrcl  10632  frecuzrdgsuc  10636  frecuzrdgrclt  10637  frecuzrdgg  10638  frecuzrdgsuctlem  10645  seqvalcd  10683  seqovcd  10689  seq3caopr3  10713  seq3caopr2  10715  seqcaopr2g  10716  iseqf1olemqf1o  10728  seq3homo  10749  seqhomog  10752  seqfeq4g  10753  seq3distr  10754  fimaxq  11049  zfz1isolem1  11062  wrd2ind  11255  rsqrmo  11538  climcn2  11820  addcn2  11821  mulcn2  11823  fsum2dlemstep  11945  fisumcom2  11949  cvgratnn  12042  fprodcl2lem  12116  fprod2dlemstep  12133  fprodcom2fi  12137  divalglemeunn  12432  divalglemeuneg  12434  bezoutlemeu  12528  isprm6  12669  pw2dvdseu  12690  crth  12746  eulerthlemh  12753  4sqlemffi  12919  ennnfonelemim  12995  nninfdclemf1  13023  unbendc  13025  imasaddfnlemg  13347  ercpbl  13364  plusffng  13398  mgmplusf  13399  opifismgmdc  13404  issgrpd  13445  sgrppropd  13446  ismndd  13470  mndpropd  13473  issubmnd  13475  mndinvmod  13478  mhmpropd  13499  idmhm  13502  mhmf1o  13503  issubmd  13507  mndissubm  13508  submid  13510  0mhm  13519  resmhm  13520  resmhm2  13521  resmhm2b  13522  mhmco  13523  grppropd  13550  grpsubf  13612  dfgrp3m  13632  mhmmnd  13653  mhmfmhm  13654  mulgfng  13661  issubg4m  13730  grpissubg  13731  isnsg3  13744  0nsg  13751  nsgid  13752  isghmd  13789  ghmmhm  13790  idghm  13796  ghmnsgima  13805  ghmnsgpreima  13806  ghmf1  13810  kerf1ghm  13811  ghmf1o  13812  ghmcmn  13864  invghm  13866  ablnsg  13871  imasabl  13873  srgfcl  13936  srglmhm  13956  srgrmhm  13957  isrhm2d  14129  subrngringnsg  14169  issubrng2  14174  subrngintm  14176  issubrg2  14205  subrgintm  14207  aprap  14250  islmodd  14257  lmodscaf  14274  lmodprop2d  14312  islssmd  14323  islss4  14346  lsspropdg  14395  issubrgd  14416  dflidl2rng  14445  rnglidlmmgm  14460  expghmap  14571  mulgghm2  14572  znf1o  14615  znidom  14621  tgclb  14739  txbas  14932  txcnp  14945  txcnmpt  14947  cnmpt21  14965  txswaphmeo  14995  isxmetd  15021  isxmet2d  15022  xmettpos  15044  blfvalps  15059  xmetresbl  15114  metss2  15172  comet  15173  bdmet  15176  bdmopn  15178  xmetxp  15181  qtopbasss  15195  elcncf1di  15253  cncfcdm  15256  mulc1cncf  15263  cncfco  15265  dedekindeulemloc  15293  dedekindeu  15297  dedekindicclemloc  15302  dedekindicclemicc  15306  ivthinclemloc  15315  dich0  15326  dvmptfsum  15399  mpodvdsmulf1o  15664  fsumdvdsmul  15665  gausslemma2dlem1f1o  15739  lgseisenlem2  15750  lgsquadlemsfi  15754  lgsquadlem1  15756  lgsquadlem2  15757  lgsquadlem3  15758  usgredgreu  16014  uspgredg2vtxeu  16016  uspgredg2v  16019  usgredg2v  16022  sssneq  16368  exmidsbthrlem  16390  cvgcmp2n  16401  trirec0  16412  apdiff  16416  redc0  16425  reap0  16426  cndcap  16427  neap0mkv  16437