Theorem ralrimivva 2512

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 114	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓))
3	2	ralrimivv 2511	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1480  ∀wral 2414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2419

This theorem is referenced by:  swopo  4223  sosng  4607  fcof1  5677  fliftfund  5691  isoresbr  5703  isocnv  5705  f1oiso  5720  caovclg  5916  caovcomg  5919  off  5987  caofrss  5999  oprssdmm  6062  dmmpog  6100  fnmpoovd  6105  fmpoco  6106  poxp  6122  f1od2  6125  eroprf  6515  dom2lem  6659  xpf1o  6731  fidifsnid  6758  nnwetri  6797  undiffi  6806  fidcenumlemim  6833  supmoti  6873  supsnti  6885  supisoti  6890  difinfsnlem  6977  addlocpr  7337  mullocpr  7372  cauappcvgprlemloc  7453  cauappcvgprlemlim  7462  caucvgprlemloc  7476  caucvgprprlemloc  7504  suplocexprlemloc  7522  suplocsrlemb  7607  rereceu  7690  axpre-suploclemres  7702  ltordlem  8237  cju  8712  exbtwnz  10021  frec2uzf1od  10172  frec2uzisod  10173  frecuzrdgrrn  10174  frec2uzrdg  10175  frecuzrdgrcl  10176  frecuzrdgsuc  10180  frecuzrdgrclt  10181  frecuzrdgg  10182  frecuzrdgsuctlem  10189  seqvalcd  10225  seqovcd  10229  seq3caopr3  10247  seq3caopr2  10248  iseqf1olemqf1o  10259  seq3homo  10276  seq3distr  10279  fimaxq  10566  zfz1isolem1  10576  rsqrmo  10792  climcn2  11071  addcn2  11072  mulcn2  11074  fsum2dlemstep  11196  fisumcom2  11200  cvgratnn  11293  divalglemeunn  11607  divalglemeuneg  11609  bezoutlemeu  11684  isprm6  11814  pw2dvdseu  11835  crth  11889  ennnfonelemim  11926  tgclb  12223  txbas  12416  txcnp  12429  txcnmpt  12431  cnmpt21  12449  txswaphmeo  12479  isxmetd  12505  isxmet2d  12506  xmettpos  12528  blfvalps  12543  xmetresbl  12598  metss2  12656  comet  12657  bdmet  12660  bdmopn  12662  xmetxp  12665  qtopbasss  12679  elcncf1di  12724  cncffvrn  12727  mulc1cncf  12734  cncfco  12736  dedekindeulemloc  12755  dedekindeu  12759  dedekindicclemloc  12764  dedekindicclemicc  12768  ivthinclemloc  12777  exmidsbthrlem  13206  cvgcmp2n  13217