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 418 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜓))) |
3 | 2 | ralrimdv 3190 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜓)) |
4 | 3 | ralrimiv 3183 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∈ wcel 2114 ∀wral 3140 |
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 209 df-an 399 df-ral 3145 |
This theorem is referenced by: ralrimivva 3193 ralrimdvv 3195 reuind 3746 disjiund 5058 disjxiun 5065 somo 5512 ssrel2 5661 sorpsscmpl 7462 f1o2ndf1 7820 soxp 7825 smoiso 8001 smo11 8003 fiint 8797 sornom 9701 axdc4lem 9879 zorn2lem6 9925 fpwwe2lem12 10065 fpwwe2lem13 10066 nqereu 10353 genpnnp 10429 receu 11287 lbreu 11593 injresinj 13161 sqrmo 14613 iscatd 16946 isfuncd 17137 0subm 17984 insubm 17985 sursubmefmnd 18063 injsubmefmnd 18064 cycsubm 18347 symgextf1 18551 lsmsubm 18780 iscmnd 18921 qusabl 18987 cycsubmcmn 19010 dprdsubg 19148 issrngd 19634 quscrng 20015 mamudm 21001 mat1dimcrng 21088 mavmuldm 21161 fitop 21510 tgcl 21579 topbas 21582 ppttop 21617 epttop 21619 restbas 21768 isnrm2 21968 isnrm3 21969 2ndcctbss 22065 txbas 22177 txbasval 22216 txhaus 22257 xkohaus 22263 basqtop 22321 opnfbas 22452 isfild 22468 filfi 22469 neifil 22490 fbasrn 22494 filufint 22530 rnelfmlem 22562 fmfnfmlem3 22566 fmfnfm 22568 blfps 23018 blf 23019 blbas 23042 minveclem3b 24033 aalioulem2 24924 axcontlem9 26760 upgrwlkdvdelem 27519 grpodivf 28317 ipf 28492 ocsh 29062 adjadj 29715 unopadj2 29717 hmopadj 29718 hmopbdoptHIL 29767 lnopmi 29779 adjlnop 29865 xreceu 30600 esumcocn 31341 bnj1384 32306 f1resrcmplf1d 32362 mclsax 32818 dfon2 33039 nocvxmin 33250 outsideofeu 33594 hilbert1.2 33618 opnrebl2 33671 nn0prpw 33673 fness 33699 tailfb 33727 ontopbas 33778 neificl 35030 metf1o 35032 crngohomfo 35286 smprngopr 35332 ispridlc 35350 prter2 36019 snatpsubN 36888 pclclN 37029 pclfinN 37038 ltrncnv 37284 cdleme24 37490 cdleme28 37511 cdleme50ltrn 37695 cdleme 37698 ltrnco 37857 cdlemk28-3 38046 diaf11N 38187 dibf11N 38299 dihlsscpre 38372 mapdpg 38844 mapdh9a 38927 mapdh9aOLDN 38928 hdmap14lem6 39011 mzpincl 39338 mzpindd 39350 iunconnlem2 41276 islptre 41907 2reu8i 43319 lmod1 44554 |
Copyright terms: Public domain | W3C validator |