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 451 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜓))) |
3 | 2 | ralrimdv 2951 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜓)) |
4 | 3 | ralrimiv 2948 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 1977 ∀wral 2896 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ral 2901 |
This theorem is referenced by: ralrimivva 2954 ralrimdvv 2956 reuind 3378 disjxiun 4579 disjxiunOLD 4580 somo 4993 ssrel2 5133 sorpsscmpl 6846 f1o2ndf1 7172 soxp 7177 smoiso 7346 smo11 7348 fiint 8122 sornom 8982 axdc4lem 9160 zorn2lem6 9206 fpwwe2lem12 9342 fpwwe2lem13 9343 nqereu 9630 genpnnp 9706 receu 10551 lbreu 10852 injresinj 12451 sqrmo 13840 iscatd 16157 isfuncd 16348 symgextf1 17664 lsmsubm 17891 iscmnd 18028 qusabl 18091 dprdsubg 18246 issrngd 18684 quscrng 19061 mamudm 20013 mat1dimcrng 20102 mavmuldm 20175 fitop 20530 tgcl 20584 topbas 20587 ppttop 20621 epttop 20623 restbas 20772 isnrm2 20972 isnrm3 20973 2ndcctbss 21068 txbas 21180 txbasval 21219 txhaus 21260 xkohaus 21266 basqtop 21324 opnfbas 21456 isfild 21472 filfi 21473 neifil 21494 fbasrn 21498 filufint 21534 rnelfmlem 21566 fmfnfmlem3 21570 fmfnfm 21572 blfps 22021 blf 22022 blbas 22045 minveclem3b 23007 aalioulem2 23892 axcontlem9 25652 wlkdvspthlem 26137 frgrawopreglem4 26574 grpodivf 26776 ipf 26952 ocsh 27526 adjadj 28179 unopadj2 28181 hmopadj 28182 hmopbdoptHIL 28231 lnopmi 28243 adjlnop 28329 xreceu 28961 esumcocn 29469 bnj1384 30354 mclsax 30720 dfon2 30941 nocvxmin 31090 outsideofeu 31408 hilbert1.2 31432 opnrebl2 31486 nn0prpw 31488 fness 31514 tailfb 31542 ontopbas 31597 neificl 32719 metf1o 32721 crngohomfo 32975 smprngopr 33021 ispridlc 33039 prter2 33184 snatpsubN 34054 pclclN 34195 pclfinN 34204 ltrncnv 34450 cdleme24 34658 cdleme28 34679 cdleme50ltrn 34863 cdleme 34866 ltrnco 35025 cdlemk28-3 35214 diaf11N 35356 dibf11N 35468 dihlsscpre 35541 mapdpg 36013 mapdh9a 36097 mapdh9aOLDN 36098 hdmap14lem6 36183 mzpincl 36315 mzpindd 36327 iunconlem2 38193 islptre 38686 upgrwlkdvdelem 40942 frgrwopreglem4 41484 lmod1 42075 |
Copyright terms: Public domain | W3C validator |