Theorem ralrimivva 2401

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

Syntax hints:   → wi 4   ∧ wa 97   ∈ wcel 1393  ∀wral 2306

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311

This theorem is referenced by:  swopo  4043  sosng  4413  fcof1  5423  fliftfund  5437  isoresbr  5449  isocnv  5451  f1oiso  5465  caovclg  5653  caovcomg  5656  off  5724  caofrss  5735  fmpt2co  5837  poxp  5853  eroprf  6199  dom2lem  6252  nnwetri  6354  addlocpr  6634  mullocpr  6669  cauappcvgprlemloc  6750  cauappcvgprlemlim  6759  caucvgprlemloc  6773  caucvgprprlemloc  6801  rereceu  6963  cju  7913  qbtwnz  9106  frec2uzf1od  9192  frec2uzisod  9193  frecuzrdgrrn  9194  iseqcaopr3  9240  iseqcaopr2  9241  iseqhomo  9248  iseqdistr  9249  rsqrmo  9625  climcn2  9830  addcn2  9831  mulcn2  9833