![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralrimivv | Structured version Visualization version GIF version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 24-Jul-2004.) |
Ref | Expression |
---|---|
ralrimivv.1 | ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓)) |
Ref | Expression |
---|---|
ralrimivv | ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralrimivv.1 | . . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓)) | |
2 | 1 | expd 414 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜓))) |
3 | 2 | ralrimdv 3150 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜓)) |
4 | 3 | ralrimiv 3143 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∈ wcel 2104 ∀wral 3059 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ral 3060 |
This theorem is referenced by: ralrimivva 3198 ralrimdvv 3199 reuind 3748 disjiund 5137 disjxiun 5144 somo 5624 ssrel2 5784 sorpsscmpl 7726 f1o2ndf1 8110 soxp 8117 smoiso 8364 smo11 8366 fiint 9326 sornom 10274 axdc4lem 10452 zorn2lem6 10498 fpwwe2lem11 10638 fpwwe2lem12 10639 nqereu 10926 genpnnp 11002 receu 11863 lbreu 12168 injresinj 13757 sqrmo 15202 iscatd 17621 isfuncd 17819 0subm 18734 insubm 18735 sursubmefmnd 18813 injsubmefmnd 18814 cycsubm 19117 symgextf1 19330 lsmsubm 19562 iscmnd 19703 qusabl 19774 cycsubmcmn 19798 dprdsubg 19935 issrngd 20612 quscrng 21029 mamudm 22110 mat1dimcrng 22199 mavmuldm 22272 fitop 22622 tgcl 22692 topbas 22695 ppttop 22730 epttop 22732 restbas 22882 isnrm2 23082 isnrm3 23083 2ndcctbss 23179 txbas 23291 txbasval 23330 txhaus 23371 xkohaus 23377 basqtop 23435 opnfbas 23566 isfild 23582 filfi 23583 neifil 23604 fbasrn 23608 filufint 23644 rnelfmlem 23676 fmfnfmlem3 23680 fmfnfm 23682 blfps 24132 blf 24133 blbas 24156 minveclem3b 25176 aalioulem2 26082 nocvxmin 27516 negsprop 27748 axcontlem9 28497 upgrwlkdvdelem 29260 grpodivf 30058 ipf 30233 ocsh 30803 adjadj 31456 unopadj2 31458 hmopadj 31459 hmopbdoptHIL 31508 lnopmi 31520 adjlnop 31606 xreceu 32355 esumcocn 33376 bnj1384 34341 f1resrcmplf1d 34388 mclsax 34858 dfon2 35068 outsideofeu 35407 hilbert1.2 35431 opnrebl2 35509 nn0prpw 35511 fness 35537 tailfb 35565 ontopbas 35616 neificl 36924 metf1o 36926 crngohomfo 37177 smprngopr 37223 ispridlc 37241 disjdmqsss 37975 disjdmqscossss 37976 prter2 38054 snatpsubN 38924 pclclN 39065 pclfinN 39074 ltrncnv 39320 cdleme24 39526 cdleme28 39547 cdleme50ltrn 39731 cdleme 39734 ltrnco 39893 cdlemk28-3 40082 diaf11N 40223 dibf11N 40335 dihlsscpre 40408 mapdpg 40880 mapdh9a 40963 mapdh9aOLDN 40964 hdmap14lem6 41047 mzpincl 41774 mzpindd 41786 iunconnlem2 43998 islptre 44633 fcoresf1 46077 2reu8i 46119 lmod1 47260 |
Copyright terms: Public domain | W3C validator |