Theorem ralrimivva 2632

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  swopo  4451  sosng  4848  fcof1  5989  fliftfund  6003  isoresbr  6015  isocnv  6017  f1oiso  6032  oveqrspc2v  6112  caovclg  6242  caovcomg  6245  off  6315  caofrss  6334  caofdig  6336  oprssdmm  6405  dmmpog  6445  fnmpoovd  6451  fmpoco  6452  poxp  6468  f1od2  6471  suppofss1dcl  6504  suppofss2dcl  6505  eroprf  6902  dom2lem  7058  xpf1o  7144  fidifsnid  7173  nnwetri  7223  undiffi  7232  fidcenumlemim  7269  supmoti  7333  supsnti  7345  supisoti  7350  difinfsnlem  7439  nninfwlpor  7514  netap  7620  2omotaplemap  7623  cc2lem  7632  addlocpr  7903  mullocpr  7938  cauappcvgprlemloc  8019  cauappcvgprlemlim  8028  caucvgprlemloc  8042  caucvgprprlemloc  8070  suplocexprlemloc  8088  suplocsrlemb  8173  rereceu  8256  axpre-suploclemres  8268  ltordlem  8811  cju  9293  exbtwnz  10695  frec2uzf1od  10856  frec2uzisod  10857  frecuzrdgrrn  10858  frec2uzrdg  10859  frecuzrdgrcl  10860  frecuzrdgsuc  10864  frecuzrdgrclt  10865  frecuzrdgg  10866  frecuzrdgsuctlem  10873  seqvalcd  10911  seqovcd  10917  seq3caopr3  10941  seq3caopr2  10943  seqcaopr2g  10944  iseqf1olemqf1o  10956  seq3homo  10977  seqhomog  10980  seqfeq4g  10981  seq3distr  10982  fimaxq  11284  zfz1isolem1  11306  wrd2ind  11509  rsqrmo  11807  climcn2  12091  addcn2  12092  mulcn2  12094  fsum2dlemstep  12217  fisumcom2  12221  cvgratnn  12314  fprodcl2lem  12388  fprod2dlemstep  12405  fprodcom2fi  12409  divalglemeunn  12704  divalglemeuneg  12706  bezoutlemeu  12800  isprm6  12942  pwbdvdseu  12963  crth  13022  eulerthlemh  13029  4sqlemffi  13195  ennnfonelemim  13364  nninfdclemf1  13392  unbendc  13394  imasaddfnlemg  13684  ercpbl  13701  plusffng  13734  mgmplusf  13735  opifismgmdc  13740  issgrpd  13776  sgrppropd  13777  ismndd  13799  mndpropd  13802  issubmnd  13804  mndinvmod  13807  mhmpropd  13822  idmhm  13825  mhmf1o  13826  issubmd  13830  mndissubm  13831  submid  13833  0mhm  13842  resmhm  13843  resmhm2  13844  resmhm2b  13845  mhmco  13846  grppropd  13871  grpsubf  13933  dfgrp3m  13953  mhmmnd  13968  mhmfmhm  13969  mulgfng  13976  issubg4m  14045  grpissubg  14046  isnsg3  14059  0nsg  14066  nsgid  14067  isghmd  14104  ghmmhm  14105  idghm  14111  ghmnsgima  14120  ghmnsgpreima  14121  ghmf1  14125  kerf1ghm  14126  ghmf1o  14127  cmnsubm  14161  ghmcmn  14180  invghm  14182  ablnsg  14187  imasabl  14189  srgfcl  14326  srglmhm  14346  srgrmhm  14347  isrhm2d  14521  subrngringnsg  14562  issubrng2  14567  subrngintm  14569  issubrg2  14598  subrgintm  14600  aprap  14647  aprlring  14649  islmodd  14678  lmodscaf  14696  lmodprop2d  14734  islssmd  14745  islss4  14768  lsspropdg  14817  issubrgd  14838  dflidl2rng  14867  rnglidlmmgm  14882  expghmap  14991  mulgghm2  14992  znf1o  15035  znidom  15041  issubassa2  15084  tgclb  15215  txbas  15408  txcnp  15421  txcnmpt  15423  cnmpt21  15441  txswaphmeo  15471  isxmetd  15497  isxmet2d  15498  xmettpos  15520  blfvalps  15535  xmetresbl  15590  metss2  15648  comet  15649  bdmet  15652  bdmopn  15654  xmetxp  15657  qtopbasss  15671  elcncf1di  15729  cncfcdm  15732  mulc1cncf  15739  cncfco  15741  dedekindeulemloc  15769  dedekindeu  15773  dedekindicclemloc  15778  dedekindicclemicc  15782  ivthinclemloc  15791  dich0  15802  dvmptfsum  15875  mpodvdsmulf1o  16185  fsumdvdsmul  16186  gausslemma2dlem1f1o  16277  lgseisenlem2  16288  lgsquadlemsfi  16292  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  usgredgreu  16555  uspgredg2vtxeu  16557  uspgredg2v  16560  usgredg2v  16563  vtxedgfi  16628  vtxlpfi  16629  dichmul0or  16858  sssneq  17130  exmidsbthrlem  17165  cvgcmp2n  17180  trirec0  17191  apdiff  17195  redc0  17205  reap0  17206  cndcap  17207  neap0mkv  17217