Theorem ralrimivva 2615

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  ∀wral 2511

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516

This theorem is referenced by:  swopo  4409  sosng  4805  fcof1  5934  fliftfund  5948  isoresbr  5960  isocnv  5962  f1oiso  5977  oveqrspc2v  6055  caovclg  6185  caovcomg  6188  off  6257  caofrss  6276  caofdig  6278  oprssdmm  6343  dmmpog  6383  fnmpoovd  6389  fmpoco  6390  poxp  6406  f1od2  6409  suppofss1dcl  6442  suppofss2dcl  6443  eroprf  6840  dom2lem  6988  xpf1o  7073  fidifsnid  7101  nnwetri  7151  undiffi  7160  fidcenumlemim  7194  supmoti  7252  supsnti  7264  supisoti  7269  difinfsnlem  7358  nninfwlpor  7433  netap  7533  2omotaplemap  7536  cc2lem  7545  addlocpr  7816  mullocpr  7851  cauappcvgprlemloc  7932  cauappcvgprlemlim  7941  caucvgprlemloc  7955  caucvgprprlemloc  7983  suplocexprlemloc  8001  suplocsrlemb  8086  rereceu  8169  axpre-suploclemres  8181  ltordlem  8721  cju  9200  exbtwnz  10573  frec2uzf1od  10731  frec2uzisod  10732  frecuzrdgrrn  10733  frec2uzrdg  10734  frecuzrdgrcl  10735  frecuzrdgsuc  10739  frecuzrdgrclt  10740  frecuzrdgg  10741  frecuzrdgsuctlem  10748  seqvalcd  10786  seqovcd  10792  seq3caopr3  10816  seq3caopr2  10818  seqcaopr2g  10819  iseqf1olemqf1o  10831  seq3homo  10852  seqhomog  10855  seqfeq4g  10856  seq3distr  10857  fimaxq  11154  zfz1isolem1  11167  wrd2ind  11370  rsqrmo  11667  climcn2  11949  addcn2  11950  mulcn2  11952  fsum2dlemstep  12075  fisumcom2  12079  cvgratnn  12172  fprodcl2lem  12246  fprod2dlemstep  12263  fprodcom2fi  12267  divalglemeunn  12562  divalglemeuneg  12564  bezoutlemeu  12658  isprm6  12799  pw2dvdseu  12820  crth  12876  eulerthlemh  12883  4sqlemffi  13049  ennnfonelemim  13125  nninfdclemf1  13153  unbendc  13155  imasaddfnlemg  13477  ercpbl  13494  plusffng  13528  mgmplusf  13529  opifismgmdc  13534  issgrpd  13575  sgrppropd  13576  ismndd  13600  mndpropd  13603  issubmnd  13605  mndinvmod  13608  mhmpropd  13629  idmhm  13632  mhmf1o  13633  issubmd  13637  mndissubm  13638  submid  13640  0mhm  13649  resmhm  13650  resmhm2  13651  resmhm2b  13652  mhmco  13653  grppropd  13680  grpsubf  13742  dfgrp3m  13762  mhmmnd  13783  mhmfmhm  13784  mulgfng  13791  issubg4m  13860  grpissubg  13861  isnsg3  13874  0nsg  13881  nsgid  13882  isghmd  13919  ghmmhm  13920  idghm  13926  ghmnsgima  13935  ghmnsgpreima  13936  ghmf1  13940  kerf1ghm  13941  ghmf1o  13942  ghmcmn  13994  invghm  13996  ablnsg  14001  imasabl  14003  srgfcl  14067  srglmhm  14087  srgrmhm  14088  isrhm2d  14260  subrngringnsg  14300  issubrng2  14305  subrngintm  14307  issubrg2  14336  subrgintm  14338  aprap  14382  islmodd  14389  lmodscaf  14406  lmodprop2d  14444  islssmd  14455  islss4  14478  lsspropdg  14527  issubrgd  14548  dflidl2rng  14577  rnglidlmmgm  14592  expghmap  14703  mulgghm2  14704  znf1o  14747  znidom  14753  tgclb  14876  txbas  15069  txcnp  15082  txcnmpt  15084  cnmpt21  15102  txswaphmeo  15132  isxmetd  15158  isxmet2d  15159  xmettpos  15181  blfvalps  15196  xmetresbl  15251  metss2  15309  comet  15310  bdmet  15313  bdmopn  15315  xmetxp  15318  qtopbasss  15332  elcncf1di  15390  cncfcdm  15393  mulc1cncf  15400  cncfco  15402  dedekindeulemloc  15430  dedekindeu  15434  dedekindicclemloc  15439  dedekindicclemicc  15443  ivthinclemloc  15452  dich0  15463  dvmptfsum  15536  mpodvdsmulf1o  15804  fsumdvdsmul  15805  gausslemma2dlem1f1o  15879  lgseisenlem2  15890  lgsquadlemsfi  15894  lgsquadlem1  15896  lgsquadlem2  15897  lgsquadlem3  15898  usgredgreu  16157  uspgredg2vtxeu  16159  uspgredg2v  16162  usgredg2v  16165  vtxedgfi  16230  vtxlpfi  16231  sssneq  16724  exmidsbthrlem  16750  cvgcmp2n  16765  trirec0  16776  apdiff  16780  redc0  16790  reap0  16791  cndcap  16792  neap0mkv  16802