![]() |
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 415 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜓))) |
3 | 2 | ralrimdv 3151 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜓)) |
4 | 3 | ralrimiv 3144 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2105 ∀wral 3060 |
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 1912 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ral 3061 |
This theorem is referenced by: ralrimivva 3199 ralrimdvv 3200 reuind 3749 disjiund 5138 disjxiun 5145 somo 5625 ssrel2 5785 sorpsscmpl 7728 f1o2ndf1 8112 soxp 8119 smoiso 8366 smo11 8368 fiint 9328 sornom 10276 axdc4lem 10454 zorn2lem6 10500 fpwwe2lem11 10640 fpwwe2lem12 10641 nqereu 10928 genpnnp 11004 receu 11864 lbreu 12169 injresinj 13758 sqrmo 15203 iscatd 17622 isfuncd 17820 0subm 18735 insubm 18736 sursubmefmnd 18814 injsubmefmnd 18815 cycsubm 19118 symgextf1 19331 lsmsubm 19563 iscmnd 19704 qusabl 19775 cycsubmcmn 19799 dprdsubg 19936 issrngd 20613 quscrng 21030 mamudm 22111 mat1dimcrng 22200 mavmuldm 22273 fitop 22623 tgcl 22693 topbas 22696 ppttop 22731 epttop 22733 restbas 22883 isnrm2 23083 isnrm3 23084 2ndcctbss 23180 txbas 23292 txbasval 23331 txhaus 23372 xkohaus 23378 basqtop 23436 opnfbas 23567 isfild 23583 filfi 23584 neifil 23605 fbasrn 23609 filufint 23645 rnelfmlem 23677 fmfnfmlem3 23681 fmfnfm 23683 blfps 24133 blf 24134 blbas 24157 minveclem3b 25177 aalioulem2 26083 nocvxmin 27517 negsprop 27749 axcontlem9 28498 upgrwlkdvdelem 29261 grpodivf 30059 ipf 30234 ocsh 30804 adjadj 31457 unopadj2 31459 hmopadj 31460 hmopbdoptHIL 31509 lnopmi 31521 adjlnop 31607 xreceu 32356 esumcocn 33377 bnj1384 34342 f1resrcmplf1d 34389 mclsax 34859 dfon2 35069 outsideofeu 35408 hilbert1.2 35432 opnrebl2 35510 nn0prpw 35512 fness 35538 tailfb 35566 ontopbas 35617 neificl 36925 metf1o 36927 crngohomfo 37178 smprngopr 37224 ispridlc 37242 disjdmqsss 37976 disjdmqscossss 37977 prter2 38055 snatpsubN 38925 pclclN 39066 pclfinN 39075 ltrncnv 39321 cdleme24 39527 cdleme28 39548 cdleme50ltrn 39732 cdleme 39735 ltrnco 39894 cdlemk28-3 40083 diaf11N 40224 dibf11N 40336 dihlsscpre 40409 mapdpg 40881 mapdh9a 40964 mapdh9aOLDN 40965 hdmap14lem6 41048 mzpincl 41775 mzpindd 41787 iunconnlem2 43999 islptre 44634 fcoresf1 46078 2reu8i 46120 lmod1 47261 |
Copyright terms: Public domain | W3C validator |