Theorem ralrimivv 3175

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 24-Jul-2004.)

Hypothesis

Ref	Expression
ralrimivv.1	⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓))

Assertion

Ref	Expression
ralrimivv	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Distinct variable groups:   𝑥,𝑦,𝜑   𝑦,𝐴

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem ralrimivv

Step	Hyp	Ref	Expression
1		ralrimivv.1	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓))
2	1	expd 415	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜓)))
3	2	ralrimdv 3132	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜓))
4	3	ralrimiv 3125	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∀wral 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3050

This theorem is referenced by:  ralrimivva  3177  ralrimdvv  3178  reuind  3709  disjiund  5086  disjxiun  5092  somo  5568  ssrel2  5731  sorpsscmpl  7676  resf1extb  7873  f1o2ndf1  8061  soxp  8068  smoiso  8291  smo11  8293  fiint  9221  sornom  10178  axdc4lem  10356  zorn2lem6  10402  fpwwe2lem11  10542  fpwwe2lem12  10543  nqereu  10830  genpnnp  10906  receu  11772  lbreu  12082  injresinj  13701  sqrmo  15168  iscatd  17589  isfuncd  17782  0subm  18735  insubm  18736  sursubmefmnd  18814  injsubmefmnd  18815  cycsubm  19124  symgextf1  19343  lsmsubm  19575  iscmnd  19716  qusabl  19787  cycsubmcmn  19811  dprdsubg  19948  issrngd  20780  quscrng  21230  mamudm  22320  mat1dimcrng  22402  mavmuldm  22475  fitop  22825  tgcl  22894  topbas  22897  ppttop  22932  epttop  22934  restbas  23083  isnrm2  23283  isnrm3  23284  2ndcctbss  23380  txbas  23492  txbasval  23531  txhaus  23572  xkohaus  23578  basqtop  23636  opnfbas  23767  isfild  23783  filfi  23784  neifil  23805  fbasrn  23809  filufint  23845  rnelfmlem  23877  fmfnfmlem3  23881  fmfnfm  23883  blfps  24331  blf  24332  blbas  24355  minveclem3b  25365  aalioulem2  26278  nocvxmin  27728  negsprop  27987  axcontlem9  28961  upgrwlkdvdelem  29725  grpodivf  30529  ipf  30704  ocsh  31274  adjadj  31927  unopadj2  31929  hmopadj  31930  hmopbdoptHIL  31979  lnopmi  31991  adjlnop  32077  xreceu  32913  esumcocn  34104  bnj1384  35055  f1resrcmplf1d  35110  mclsax  35624  dfon2  35845  outsideofeu  36186  hilbert1.2  36210  opnrebl2  36376  nn0prpw  36378  fness  36404  tailfb  36432  ontopbas  36483  neificl  37803  metf1o  37805  crngohomfo  38056  smprngopr  38102  ispridlc  38120  disjdmqsss  38910  disjdmqscossss  38911  prter2  38990  snatpsubN  39859  pclclN  40000  pclfinN  40009  ltrncnv  40255  cdleme24  40461  cdleme28  40482  cdleme50ltrn  40666  cdleme  40669  ltrnco  40828  cdlemk28-3  41017  diaf11N  41158  dibf11N  41270  dihlsscpre  41343  mapdpg  41815  mapdh9a  41898  mapdh9aOLDN  41899  hdmap14lem6  41982  mzpincl  42841  mzpindd  42853  iunconnlem2  45041  islptre  45733  ormkglobd  46987  fcoresf1  47183  2reu8i  47227  lmod1  48607