Theorem ralrimivva 2473

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1448  ∀wral 2375

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-4 1455  ax-17 1474

This theorem depends on definitions:  df-bi 116  df-nf 1405  df-ral 2380

This theorem is referenced by:  swopo  4166  sosng  4550  fcof1  5616  fliftfund  5630  isoresbr  5642  isocnv  5644  f1oiso  5659  caovclg  5855  caovcomg  5858  off  5926  caofrss  5937  dmmpog  6037  fnmpoovd  6042  fmpoco  6043  poxp  6059  f1od2  6062  eroprf  6452  dom2lem  6596  xpf1o  6667  fidifsnid  6694  nnwetri  6733  undiffi  6742  fidcenumlemim  6768  supmoti  6795  supsnti  6807  supisoti  6812  difinfsnlem  6899  addlocpr  7245  mullocpr  7280  cauappcvgprlemloc  7361  cauappcvgprlemlim  7370  caucvgprlemloc  7384  caucvgprprlemloc  7412  rereceu  7574  ltordlem  8111  cju  8577  exbtwnz  9869  frec2uzf1od  10020  frec2uzisod  10021  frecuzrdgrrn  10022  frec2uzrdg  10023  frecuzrdgrcl  10024  frecuzrdgsuc  10028  frecuzrdgrclt  10029  frecuzrdgg  10030  frecuzrdgsuctlem  10037  seqvalcd  10073  seqovcd  10077  seq3caopr3  10095  seq3caopr2  10096  iseqf1olemqf1o  10107  seq3homo  10124  seq3distr  10127  fimaxq  10414  zfz1isolem1  10424  rsqrmo  10639  climcn2  10917  addcn2  10918  mulcn2  10920  fsum2dlemstep  11042  fisumcom2  11046  cvgratnn  11139  divalglemeunn  11413  divalglemeuneg  11415  bezoutlemeu  11488  isprm6  11618  pw2dvdseu  11638  crth  11692  ennnfonelemim  11729  tgclb  12016  txbas  12208  txcnp  12221  txcnmpt  12223  cnmpt21  12241  isxmetd  12275  isxmet2d  12276  xmettpos  12298  blfvalps  12313  xmetresbl  12368  metss2  12426  comet  12427  bdmet  12430  bdmopn  12432  qtopbasss  12443  elcncf1di  12479  cncffvrn  12482  mulc1cncf  12489  cncfco  12491  exmidsbthrlem  12801  cvgcmp2n  12812