Theorem ralrimivv 3205

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3079

This theorem is used by:  ralrimivva  3207  ralrimdvv  3208  reuind  3714  disjiund  5098  disjxiun  5104  somo  5606  ssrel2  5769  f1resrcmplf1d  7275  sorpsscmpl  7738  resf1extb  7934  f1o2ndf1  8122  soxp  8130  smoiso  8354  smo11  8356  fiint  9299  sornom  10282  axdc4lem  10460  zorn2lem6  10506  fpwwe2lem11  10653  fpwwe2lem12  10654  nqereu  10941  genpnnp  11017  receu  11886  lbreu  12192  injresinj  13849  sqrmo  15340  iscatd  17765  isfuncd  17958  0subm  18927  insubm  18928  sursubmefmnd  19006  injsubmefmnd  19007  cycsubm  19331  symgextf1  19549  lsmsubm  19781  iscmnd  19922  qusabl  19993  cycsubmcmn  20017  dprdsubg  20154  crngrhmfo  20638  issrngd  21022  quscrng  21487  mamudm  22618  mat1dimcrng  22700  mavmuldm  22773  fitop  23126  tgcl  23195  topbas  23198  ppttop  23233  epttop  23235  restbas  23384  isnrm2  23584  isnrm3  23585  2ndcctbss  23682  txbas  23794  txbasval  23833  txhaus  23874  xkohaus  23880  basqtop  23938  opnfbas  24069  isfild  24085  filfi  24086  neifil  24107  fbasrn  24111  filufint  24147  rnelfmlem  24179  fmfnfmlem3  24183  fmfnfm  24185  blfps  24633  blf  24634  blbas  24657  minveclem3b  25657  aalioulem2  26566  nocvxmin  28018  negsprop  28298  axcontlem9  29415  upgrwlkdvdelem  30187  grpodivf  31005  ipf  31180  ocsh  31750  adjadj  32403  unopadj2  32405  hmopadj  32406  hmopbdoptHIL  32455  lnopmi  32467  adjlnop  32553  xreceu  33354  esumcocn  34577  bnj1384  35528  mclsax  36135  dfon2  36356  outsideofeu  36698  hilbert1.2  36722  opnrebl2  36927  nn0prpw  36929  fness  36955  tailfb  36983  ontopbas  37034  neificl  38490  metf1o  38492  crngohomfo  38743  smprngopr  38789  ispridlc  38807  disjdmqsss  39640  disjdmqscossss  39641  eldisjs6  39675  prter2  39741  snatpsubN  40610  pclclN  40751  pclfinN  40760  ltrncnv  41006  cdleme24  41212  cdleme28  41233  cdleme50ltrn  41417  cdleme  41420  ltrnco  41579  cdlemk28-3  41768  diaf11N  41909  dibf11N  42021  dihlsscpre  42094  mapdpg  42566  mapdh9a  42649  mapdh9aOLDN  42650  hdmap14lem6  42733  mzpincl  43566  mzpindd  43578  iunconnlem2  45744  islptre  46436  ormkglobd  47692  fcoresf1  47944  2reu8i  47988  smprngprmrng  49241  lmod1  49409