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  4308  sosng  4701  fcof1  5786  fliftfund  5800  isoresbr  5812  isocnv  5814  f1oiso  5829  oveqrspc2v  5904  caovclg  6029  caovcomg  6032  off  6097  caofrss  6109  oprssdmm  6174  dmmpog  6212  fnmpoovd  6218  fmpoco  6219  poxp  6235  f1od2  6238  eroprf  6630  dom2lem  6774  xpf1o  6846  fidifsnid  6873  nnwetri  6917  undiffi  6926  fidcenumlemim  6953  supmoti  6994  supsnti  7006  supisoti  7011  difinfsnlem  7100  nninfwlpor  7174  netap  7255  2omotaplemap  7258  cc2lem  7267  addlocpr  7537  mullocpr  7572  cauappcvgprlemloc  7653  cauappcvgprlemlim  7662  caucvgprlemloc  7676  caucvgprprlemloc  7704  suplocexprlemloc  7722  suplocsrlemb  7807  rereceu  7890  axpre-suploclemres  7902  ltordlem  8441  cju  8920  exbtwnz  10253  frec2uzf1od  10408  frec2uzisod  10409  frecuzrdgrrn  10410  frec2uzrdg  10411  frecuzrdgrcl  10412  frecuzrdgsuc  10416  frecuzrdgrclt  10417  frecuzrdgg  10418  frecuzrdgsuctlem  10425  seqvalcd  10461  seqovcd  10465  seq3caopr3  10483  seq3caopr2  10484  iseqf1olemqf1o  10495  seq3homo  10512  seq3distr  10515  fimaxq  10809  zfz1isolem1  10822  rsqrmo  11038  climcn2  11319  addcn2  11320  mulcn2  11322  fsum2dlemstep  11444  fisumcom2  11448  cvgratnn  11541  fprodcl2lem  11615  fprod2dlemstep  11632  fprodcom2fi  11636  divalglemeunn  11928  divalglemeuneg  11930  bezoutlemeu  12010  isprm6  12149  pw2dvdseu  12170  crth  12226  eulerthlemh  12233  ennnfonelemim  12427  nninfdclemf1  12455  unbendc  12457  imasaddfnlemg  12740  ercpbl  12755  plusffng  12789  mgmplusf  12790  opifismgmdc  12795  ismndd  12843  mndpropd  12846  issubmnd  12848  mndinvmod  12851  mhmpropd  12862  idmhm  12865  mhmf1o  12866  issubmd  12870  mndissubm  12871  submid  12873  0mhm  12878  mhmco  12879  grppropd  12898  grpsubf  12954  dfgrp3m  12974  mhmmnd  12985  mhmfmhm  12986  mulgfng  12992  issubg4m  13058  grpissubg  13059  isnsg3  13072  0nsg  13079  nsgid  13080  srgfcl  13161  srglmhm  13181  srgrmhm  13182  issubrg2  13367  subrgintm  13369  aprap  13381  islmodd  13388  lmodscaf  13405  lmodprop2d  13443  islssmd  13451  islss4  13474  tgclb  13604  txbas  13797  txcnp  13810  txcnmpt  13812  cnmpt21  13830  txswaphmeo  13860  isxmetd  13886  isxmet2d  13887  xmettpos  13909  blfvalps  13924  xmetresbl  13979  metss2  14037  comet  14038  bdmet  14041  bdmopn  14043  xmetxp  14046  qtopbasss  14060  elcncf1di  14105  cncfcdm  14108  mulc1cncf  14115  cncfco  14117  dedekindeulemloc  14136  dedekindeu  14140  dedekindicclemloc  14145  dedekindicclemicc  14149  ivthinclemloc  14158  lgseisenlem2  14490  sssneq  14790  exmidsbthrlem  14809  cvgcmp2n  14820  trirec0  14831  apdiff  14835  redc0  14844  reap0  14845  cndcap  14846  neap0mkv  14856