![]() |
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 406 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜓))) |
3 | 2 | ralrimdv 3150 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜓)) |
4 | 3 | ralrimiv 3147 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∈ wcel 2107 ∀wral 3090 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ral 3095 |
This theorem is referenced by: ralrimivva 3153 ralrimdvv 3155 reuind 3628 disjiund 4877 disjxiun 4883 somo 5310 ssrel2 5457 sorpsscmpl 7225 f1o2ndf1 7566 soxp 7571 smoiso 7742 smo11 7744 fiint 8525 sornom 9434 axdc4lem 9612 zorn2lem6 9658 fpwwe2lem12 9798 fpwwe2lem13 9799 nqereu 10086 genpnnp 10162 receu 11020 lbreu 11327 injresinj 12908 sqrmo 14399 iscatd 16719 isfuncd 16910 symgextf1 18224 lsmsubm 18452 iscmnd 18591 qusabl 18654 dprdsubg 18810 issrngd 19253 quscrng 19637 mamudm 20598 mat1dimcrng 20688 mavmuldm 20761 fitop 21112 tgcl 21181 topbas 21184 ppttop 21219 epttop 21221 restbas 21370 isnrm2 21570 isnrm3 21571 2ndcctbss 21667 txbas 21779 txbasval 21818 txhaus 21859 xkohaus 21865 basqtop 21923 opnfbas 22054 isfild 22070 filfi 22071 neifil 22092 fbasrn 22096 filufint 22132 rnelfmlem 22164 fmfnfmlem3 22168 fmfnfm 22170 blfps 22619 blf 22620 blbas 22643 minveclem3b 23634 aalioulem2 24525 axcontlem9 26321 upgrwlkdvdelem 27088 grpodivf 27965 ipf 28140 ocsh 28714 adjadj 29367 unopadj2 29369 hmopadj 29370 hmopbdoptHIL 29419 lnopmi 29431 adjlnop 29517 xreceu 30192 esumcocn 30740 bnj1384 31699 mclsax 32065 dfon2 32285 nocvxmin 32483 outsideofeu 32827 hilbert1.2 32851 opnrebl2 32904 nn0prpw 32906 fness 32932 tailfb 32960 ontopbas 33010 neificl 34173 metf1o 34175 crngohomfo 34429 smprngopr 34475 ispridlc 34493 prter2 35035 snatpsubN 35904 pclclN 36045 pclfinN 36054 ltrncnv 36300 cdleme24 36506 cdleme28 36527 cdleme50ltrn 36711 cdleme 36714 ltrnco 36873 cdlemk28-3 37062 diaf11N 37203 dibf11N 37315 dihlsscpre 37388 mapdpg 37860 mapdh9a 37943 mapdh9aOLDN 37944 hdmap14lem6 38027 mzpincl 38257 mzpindd 38269 iunconnlem2 40104 islptre 40759 2reu8i 42154 lmod1 43296 |
Copyright terms: Public domain | W3C validator |