Theorem ralrimivv 3190

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 3144	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜓))
4	3	ralrimiv 3137	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2098  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3054

This theorem is referenced by:  ralrimivva  3192  ralrimdvv  3193  reuind  3741  disjiund  5128  disjxiun  5135  somo  5615  ssrel2  5775  sorpsscmpl  7717  f1o2ndf1  8102  soxp  8109  smoiso  8357  smo11  8359  fiint  9319  sornom  10267  axdc4lem  10445  zorn2lem6  10491  fpwwe2lem11  10631  fpwwe2lem12  10632  nqereu  10919  genpnnp  10995  receu  11855  lbreu  12160  injresinj  13749  sqrmo  15194  iscatd  17615  isfuncd  17813  0subm  18731  insubm  18732  sursubmefmnd  18810  injsubmefmnd  18811  cycsubm  19117  symgextf1  19330  lsmsubm  19562  iscmnd  19703  qusabl  19774  cycsubmcmn  19798  dprdsubg  19935  issrngd  20693  quscrng  21127  mamudm  22211  mat1dimcrng  22300  mavmuldm  22373  fitop  22723  tgcl  22793  topbas  22796  ppttop  22831  epttop  22833  restbas  22983  isnrm2  23183  isnrm3  23184  2ndcctbss  23280  txbas  23392  txbasval  23431  txhaus  23472  xkohaus  23478  basqtop  23536  opnfbas  23667  isfild  23683  filfi  23684  neifil  23705  fbasrn  23709  filufint  23745  rnelfmlem  23777  fmfnfmlem3  23781  fmfnfm  23783  blfps  24233  blf  24234  blbas  24257  minveclem3b  25277  aalioulem2  26186  nocvxmin  27626  negsprop  27862  axcontlem9  28665  upgrwlkdvdelem  29428  grpodivf  30226  ipf  30401  ocsh  30971  adjadj  31624  unopadj2  31626  hmopadj  31627  hmopbdoptHIL  31676  lnopmi  31688  adjlnop  31774  xreceu  32521  esumcocn  33533  bnj1384  34498  f1resrcmplf1d  34545  mclsax  35015  dfon2  35225  outsideofeu  35564  hilbert1.2  35588  opnrebl2  35662  nn0prpw  35664  fness  35690  tailfb  35718  ontopbas  35769  neificl  37077  metf1o  37079  crngohomfo  37330  smprngopr  37376  ispridlc  37394  disjdmqsss  38128  disjdmqscossss  38129  prter2  38207  snatpsubN  39077  pclclN  39218  pclfinN  39227  ltrncnv  39473  cdleme24  39679  cdleme28  39700  cdleme50ltrn  39884  cdleme  39887  ltrnco  40046  cdlemk28-3  40235  diaf11N  40376  dibf11N  40488  dihlsscpre  40561  mapdpg  41033  mapdh9a  41116  mapdh9aOLDN  41117  hdmap14lem6  41200  mzpincl  41927  mzpindd  41939  iunconnlem2  44151  islptre  44786  fcoresf1  46230  2reu8i  46272  lmod1  47327