![]() |
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 419 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜓))) |
3 | 2 | ralrimdv 3153 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜓)) |
4 | 3 | ralrimiv 3148 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2111 ∀wral 3106 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ral 3111 |
This theorem is referenced by: ralrimivva 3156 ralrimdvv 3158 reuind 3692 disjiund 5020 disjxiun 5027 somo 5474 ssrel2 5623 sorpsscmpl 7440 f1o2ndf1 7801 soxp 7806 smoiso 7982 smo11 7984 fiint 8779 sornom 9688 axdc4lem 9866 zorn2lem6 9912 fpwwe2lem12 10052 fpwwe2lem13 10053 nqereu 10340 genpnnp 10416 receu 11274 lbreu 11578 injresinj 13153 sqrmo 14603 iscatd 16936 isfuncd 17127 0subm 17974 insubm 17975 sursubmefmnd 18053 injsubmefmnd 18054 cycsubm 18337 symgextf1 18541 lsmsubm 18770 iscmnd 18911 qusabl 18978 cycsubmcmn 19001 dprdsubg 19139 issrngd 19625 quscrng 20006 mamudm 20995 mat1dimcrng 21082 mavmuldm 21155 fitop 21505 tgcl 21574 topbas 21577 ppttop 21612 epttop 21614 restbas 21763 isnrm2 21963 isnrm3 21964 2ndcctbss 22060 txbas 22172 txbasval 22211 txhaus 22252 xkohaus 22258 basqtop 22316 opnfbas 22447 isfild 22463 filfi 22464 neifil 22485 fbasrn 22489 filufint 22525 rnelfmlem 22557 fmfnfmlem3 22561 fmfnfm 22563 blfps 23013 blf 23014 blbas 23037 minveclem3b 24032 aalioulem2 24929 axcontlem9 26766 upgrwlkdvdelem 27525 grpodivf 28321 ipf 28496 ocsh 29066 adjadj 29719 unopadj2 29721 hmopadj 29722 hmopbdoptHIL 29771 lnopmi 29783 adjlnop 29869 xreceu 30624 esumcocn 31449 bnj1384 32414 f1resrcmplf1d 32470 mclsax 32929 dfon2 33150 nocvxmin 33361 outsideofeu 33705 hilbert1.2 33729 opnrebl2 33782 nn0prpw 33784 fness 33810 tailfb 33838 ontopbas 33889 neificl 35191 metf1o 35193 crngohomfo 35444 smprngopr 35490 ispridlc 35508 prter2 36177 snatpsubN 37046 pclclN 37187 pclfinN 37196 ltrncnv 37442 cdleme24 37648 cdleme28 37669 cdleme50ltrn 37853 cdleme 37856 ltrnco 38015 cdlemk28-3 38204 diaf11N 38345 dibf11N 38457 dihlsscpre 38530 mapdpg 39002 mapdh9a 39085 mapdh9aOLDN 39086 hdmap14lem6 39169 mzpincl 39675 mzpindd 39687 iunconnlem2 41641 islptre 42261 2reu8i 43669 lmod1 44901 |
Copyright terms: Public domain | W3C validator |