Theorem ralrimivva 2559

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  ∀wral 2455

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  swopo  4307  sosng  4700  fcof1  5784  fliftfund  5798  isoresbr  5810  isocnv  5812  f1oiso  5827  oveqrspc2v  5902  caovclg  6027  caovcomg  6030  off  6095  caofrss  6107  oprssdmm  6172  dmmpog  6210  fnmpoovd  6216  fmpoco  6217  poxp  6233  f1od2  6236  eroprf  6628  dom2lem  6772  xpf1o  6844  fidifsnid  6871  nnwetri  6915  undiffi  6924  fidcenumlemim  6951  supmoti  6992  supsnti  7004  supisoti  7009  difinfsnlem  7098  nninfwlpor  7172  netap  7253  2omotaplemap  7256  cc2lem  7265  addlocpr  7535  mullocpr  7570  cauappcvgprlemloc  7651  cauappcvgprlemlim  7660  caucvgprlemloc  7674  caucvgprprlemloc  7702  suplocexprlemloc  7720  suplocsrlemb  7805  rereceu  7888  axpre-suploclemres  7900  ltordlem  8439  cju  8918  exbtwnz  10251  frec2uzf1od  10406  frec2uzisod  10407  frecuzrdgrrn  10408  frec2uzrdg  10409  frecuzrdgrcl  10410  frecuzrdgsuc  10414  frecuzrdgrclt  10415  frecuzrdgg  10416  frecuzrdgsuctlem  10423  seqvalcd  10459  seqovcd  10463  seq3caopr3  10481  seq3caopr2  10482  iseqf1olemqf1o  10493  seq3homo  10510  seq3distr  10513  fimaxq  10807  zfz1isolem1  10820  rsqrmo  11036  climcn2  11317  addcn2  11318  mulcn2  11320  fsum2dlemstep  11442  fisumcom2  11446  cvgratnn  11539  fprodcl2lem  11613  fprod2dlemstep  11630  fprodcom2fi  11634  divalglemeunn  11926  divalglemeuneg  11928  bezoutlemeu  12008  isprm6  12147  pw2dvdseu  12168  crth  12224  eulerthlemh  12231  ennnfonelemim  12425  nninfdclemf1  12453  unbendc  12455  imasaddfnlemg  12735  ercpbl  12750  plusffng  12784  mgmplusf  12785  opifismgmdc  12790  ismndd  12838  mndpropd  12841  issubmnd  12843  mndinvmod  12846  mhmpropd  12857  idmhm  12860  mhmf1o  12861  issubmd  12865  mndissubm  12866  submid  12868  0mhm  12873  mhmco  12874  grppropd  12893  grpsubf  12949  dfgrp3m  12969  mhmmnd  12980  mhmfmhm  12981  mulgfng  12987  issubg4m  13053  grpissubg  13054  isnsg3  13067  0nsg  13074  nsgid  13075  srgfcl  13156  srglmhm  13176  srgrmhm  13177  issubrg2  13362  subrgintm  13364  aprap  13376  islmodd  13383  lmodscaf  13400  lmodprop2d  13438  tgclb  13568  txbas  13761  txcnp  13774  txcnmpt  13776  cnmpt21  13794  txswaphmeo  13824  isxmetd  13850  isxmet2d  13851  xmettpos  13873  blfvalps  13888  xmetresbl  13943  metss2  14001  comet  14002  bdmet  14005  bdmopn  14007  xmetxp  14010  qtopbasss  14024  elcncf1di  14069  cncfcdm  14072  mulc1cncf  14079  cncfco  14081  dedekindeulemloc  14100  dedekindeu  14104  dedekindicclemloc  14109  dedekindicclemicc  14113  ivthinclemloc  14122  lgseisenlem2  14454  sssneq  14754  exmidsbthrlem  14773  cvgcmp2n  14784  trirec0  14795  apdiff  14799  redc0  14808  reap0  14809  neap0mkv  14819