![]() |
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 3144 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜓)) |
4 | 3 | ralrimiv 3137 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2098 ∀wral 3053 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ral 3054 |
This theorem is referenced by: ralrimivva 3192 ralrimdvv 3193 reuind 3741 disjiund 5128 disjxiun 5135 somo 5615 ssrel2 5775 sorpsscmpl 7717 f1o2ndf1 8102 soxp 8109 smoiso 8357 smo11 8359 fiint 9319 sornom 10267 axdc4lem 10445 zorn2lem6 10491 fpwwe2lem11 10631 fpwwe2lem12 10632 nqereu 10919 genpnnp 10995 receu 11855 lbreu 12160 injresinj 13749 sqrmo 15194 iscatd 17615 isfuncd 17813 0subm 18731 insubm 18732 sursubmefmnd 18810 injsubmefmnd 18811 cycsubm 19117 symgextf1 19330 lsmsubm 19562 iscmnd 19703 qusabl 19774 cycsubmcmn 19798 dprdsubg 19935 issrngd 20693 quscrng 21127 mamudm 22211 mat1dimcrng 22300 mavmuldm 22373 fitop 22723 tgcl 22793 topbas 22796 ppttop 22831 epttop 22833 restbas 22983 isnrm2 23183 isnrm3 23184 2ndcctbss 23280 txbas 23392 txbasval 23431 txhaus 23472 xkohaus 23478 basqtop 23536 opnfbas 23667 isfild 23683 filfi 23684 neifil 23705 fbasrn 23709 filufint 23745 rnelfmlem 23777 fmfnfmlem3 23781 fmfnfm 23783 blfps 24233 blf 24234 blbas 24257 minveclem3b 25277 aalioulem2 26186 nocvxmin 27626 negsprop 27862 axcontlem9 28665 upgrwlkdvdelem 29428 grpodivf 30226 ipf 30401 ocsh 30971 adjadj 31624 unopadj2 31626 hmopadj 31627 hmopbdoptHIL 31676 lnopmi 31688 adjlnop 31774 xreceu 32521 esumcocn 33533 bnj1384 34498 f1resrcmplf1d 34545 mclsax 35015 dfon2 35225 outsideofeu 35564 hilbert1.2 35588 opnrebl2 35662 nn0prpw 35664 fness 35690 tailfb 35718 ontopbas 35769 neificl 37077 metf1o 37079 crngohomfo 37330 smprngopr 37376 ispridlc 37394 disjdmqsss 38128 disjdmqscossss 38129 prter2 38207 snatpsubN 39077 pclclN 39218 pclfinN 39227 ltrncnv 39473 cdleme24 39679 cdleme28 39700 cdleme50ltrn 39884 cdleme 39887 ltrnco 40046 cdlemk28-3 40235 diaf11N 40376 dibf11N 40488 dihlsscpre 40561 mapdpg 41033 mapdh9a 41116 mapdh9aOLDN 41117 hdmap14lem6 41200 mzpincl 41927 mzpindd 41939 iunconnlem2 44151 islptre 44786 fcoresf1 46230 2reu8i 46272 lmod1 47327 |
Copyright terms: Public domain | W3C validator |