|   | 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 2107 ∀wral 3060 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ral 3061 | 
| This theorem is referenced by: ralrimivva 3201 ralrimdvv 3202 reuind 3758 disjiund 5133 disjxiun 5139 somo 5630 ssrel2 5794 sorpsscmpl 7755 resf1extb 7957 f1o2ndf1 8148 soxp 8155 smoiso 8403 smo11 8405 fiint 9367 fiintOLD 9368 sornom 10318 axdc4lem 10496 zorn2lem6 10542 fpwwe2lem11 10682 fpwwe2lem12 10683 nqereu 10970 genpnnp 11046 receu 11909 lbreu 12219 injresinj 13828 sqrmo 15291 iscatd 17717 isfuncd 17911 0subm 18831 insubm 18832 sursubmefmnd 18910 injsubmefmnd 18911 cycsubm 19221 symgextf1 19440 lsmsubm 19672 iscmnd 19813 qusabl 19884 cycsubmcmn 19908 dprdsubg 20045 issrngd 20857 quscrng 21294 mamudm 22400 mat1dimcrng 22484 mavmuldm 22557 fitop 22907 tgcl 22977 topbas 22980 ppttop 23015 epttop 23017 restbas 23167 isnrm2 23367 isnrm3 23368 2ndcctbss 23464 txbas 23576 txbasval 23615 txhaus 23656 xkohaus 23662 basqtop 23720 opnfbas 23851 isfild 23867 filfi 23868 neifil 23889 fbasrn 23893 filufint 23929 rnelfmlem 23961 fmfnfmlem3 23965 fmfnfm 23967 blfps 24417 blf 24418 blbas 24441 minveclem3b 25463 aalioulem2 26376 nocvxmin 27824 negsprop 28068 axcontlem9 28988 upgrwlkdvdelem 29757 grpodivf 30558 ipf 30733 ocsh 31303 adjadj 31956 unopadj2 31958 hmopadj 31959 hmopbdoptHIL 32008 lnopmi 32020 adjlnop 32106 xreceu 32905 esumcocn 34082 bnj1384 35047 f1resrcmplf1d 35102 mclsax 35575 dfon2 35794 outsideofeu 36133 hilbert1.2 36157 opnrebl2 36323 nn0prpw 36325 fness 36351 tailfb 36379 ontopbas 36430 neificl 37761 metf1o 37763 crngohomfo 38014 smprngopr 38060 ispridlc 38078 disjdmqsss 38804 disjdmqscossss 38805 prter2 38883 snatpsubN 39753 pclclN 39894 pclfinN 39903 ltrncnv 40149 cdleme24 40355 cdleme28 40376 cdleme50ltrn 40560 cdleme 40563 ltrnco 40722 cdlemk28-3 40911 diaf11N 41052 dibf11N 41164 dihlsscpre 41237 mapdpg 41709 mapdh9a 41792 mapdh9aOLDN 41793 hdmap14lem6 41876 mzpincl 42750 mzpindd 42762 iunconnlem2 44960 islptre 45639 ormkglobd 46895 fcoresf1 47086 2reu8i 47130 lmod1 48414 | 
| Copyright terms: Public domain | W3C validator |