Theorem ralrimivva 2576

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2164  ∀wral 2472

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477

This theorem is referenced by:  swopo  4338  sosng  4733  fcof1  5827  fliftfund  5841  isoresbr  5853  isocnv  5855  f1oiso  5870  oveqrspc2v  5946  caovclg  6073  caovcomg  6076  off  6145  caofrss  6159  caofdig  6161  oprssdmm  6226  dmmpog  6264  fnmpoovd  6270  fmpoco  6271  poxp  6287  f1od2  6290  eroprf  6684  dom2lem  6828  xpf1o  6902  fidifsnid  6929  nnwetri  6974  undiffi  6983  fidcenumlemim  7013  supmoti  7054  supsnti  7066  supisoti  7071  difinfsnlem  7160  nninfwlpor  7235  netap  7316  2omotaplemap  7319  cc2lem  7328  addlocpr  7598  mullocpr  7633  cauappcvgprlemloc  7714  cauappcvgprlemlim  7723  caucvgprlemloc  7737  caucvgprprlemloc  7765  suplocexprlemloc  7783  suplocsrlemb  7868  rereceu  7951  axpre-suploclemres  7963  ltordlem  8503  cju  8982  exbtwnz  10322  frec2uzf1od  10480  frec2uzisod  10481  frecuzrdgrrn  10482  frec2uzrdg  10483  frecuzrdgrcl  10484  frecuzrdgsuc  10488  frecuzrdgrclt  10489  frecuzrdgg  10490  frecuzrdgsuctlem  10497  seqvalcd  10535  seqovcd  10541  seq3caopr3  10565  seq3caopr2  10567  seqcaopr2g  10568  iseqf1olemqf1o  10580  seq3homo  10601  seqhomog  10604  seqfeq4g  10605  seq3distr  10606  fimaxq  10901  zfz1isolem1  10914  rsqrmo  11174  climcn2  11455  addcn2  11456  mulcn2  11458  fsum2dlemstep  11580  fisumcom2  11584  cvgratnn  11677  fprodcl2lem  11751  fprod2dlemstep  11768  fprodcom2fi  11772  divalglemeunn  12065  divalglemeuneg  12067  bezoutlemeu  12147  isprm6  12288  pw2dvdseu  12309  crth  12365  eulerthlemh  12372  4sqlemffi  12537  ennnfonelemim  12584  nninfdclemf1  12612  unbendc  12614  imasaddfnlemg  12900  ercpbl  12917  plusffng  12951  mgmplusf  12952  opifismgmdc  12957  issgrpd  12998  sgrppropd  12999  ismndd  13021  mndpropd  13024  issubmnd  13026  mndinvmod  13029  mhmpropd  13041  idmhm  13044  mhmf1o  13045  issubmd  13049  mndissubm  13050  submid  13052  0mhm  13061  resmhm  13062  resmhm2  13063  resmhm2b  13064  mhmco  13065  grppropd  13092  grpsubf  13154  dfgrp3m  13174  mhmmnd  13189  mhmfmhm  13190  mulgfng  13197  issubg4m  13266  grpissubg  13267  isnsg3  13280  0nsg  13287  nsgid  13288  isghmd  13325  ghmmhm  13326  idghm  13332  ghmnsgima  13341  ghmnsgpreima  13342  ghmf1  13346  kerf1ghm  13347  ghmf1o  13348  ghmcmn  13400  invghm  13402  ablnsg  13407  imasabl  13409  srgfcl  13472  srglmhm  13492  srgrmhm  13493  isrhm2d  13664  subrngringnsg  13704  issubrng2  13709  subrngintm  13711  issubrg2  13740  subrgintm  13742  aprap  13785  islmodd  13792  lmodscaf  13809  lmodprop2d  13847  islssmd  13858  islss4  13881  lsspropdg  13930  issubrgd  13951  dflidl2rng  13980  rnglidlmmgm  13995  expghmap  14106  mulgghm2  14107  znf1o  14150  znidom  14156  tgclb  14244  txbas  14437  txcnp  14450  txcnmpt  14452  cnmpt21  14470  txswaphmeo  14500  isxmetd  14526  isxmet2d  14527  xmettpos  14549  blfvalps  14564  xmetresbl  14619  metss2  14677  comet  14678  bdmet  14681  bdmopn  14683  xmetxp  14686  qtopbasss  14700  elcncf1di  14758  cncfcdm  14761  mulc1cncf  14768  cncfco  14770  dedekindeulemloc  14798  dedekindeu  14802  dedekindicclemloc  14807  dedekindicclemicc  14811  ivthinclemloc  14820  dich0  14831  dvmptfsum  14904  gausslemma2dlem1f1o  15217  lgseisenlem2  15228  lgsquadlemsfi  15232  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  sssneq  15562  exmidsbthrlem  15582  cvgcmp2n  15593  trirec0  15604  apdiff  15608  redc0  15617  reap0  15618  cndcap  15619  neap0mkv  15629