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 452 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜓))) |
3 | 2 | ralrimdv 2968 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜓)) |
4 | 3 | ralrimiv 2965 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∈ wcel 1990 ∀wral 2912 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ral 2917 |
This theorem is referenced by: ralrimivva 2971 ralrimdvv 2973 reuind 3411 disjiund 4643 disjxiun 4649 disjxiunOLD 4650 somo 5069 ssrel2 5210 sorpsscmpl 6948 f1o2ndf1 7285 soxp 7290 smoiso 7459 smo11 7461 fiint 8237 sornom 9099 axdc4lem 9277 zorn2lem6 9323 fpwwe2lem12 9463 fpwwe2lem13 9464 nqereu 9751 genpnnp 9827 receu 10672 lbreu 10973 injresinj 12589 sqrmo 13992 iscatd 16334 isfuncd 16525 symgextf1 17841 lsmsubm 18068 iscmnd 18205 qusabl 18268 dprdsubg 18423 issrngd 18861 quscrng 19240 mamudm 20194 mat1dimcrng 20283 mavmuldm 20356 fitop 20705 tgcl 20773 topbas 20776 ppttop 20811 epttop 20813 restbas 20962 isnrm2 21162 isnrm3 21163 2ndcctbss 21258 txbas 21370 txbasval 21409 txhaus 21450 xkohaus 21456 basqtop 21514 opnfbas 21646 isfild 21662 filfi 21663 neifil 21684 fbasrn 21688 filufint 21724 rnelfmlem 21756 fmfnfmlem3 21760 fmfnfm 21762 blfps 22211 blf 22212 blbas 22235 minveclem3b 23199 aalioulem2 24088 axcontlem9 25852 upgrwlkdvdelem 26632 grpodivf 27392 ipf 27568 ocsh 28142 adjadj 28795 unopadj2 28797 hmopadj 28798 hmopbdoptHIL 28847 lnopmi 28859 adjlnop 28945 xreceu 29630 esumcocn 30142 bnj1384 31100 mclsax 31466 dfon2 31697 nocvxmin 31894 outsideofeu 32238 hilbert1.2 32262 opnrebl2 32316 nn0prpw 32318 fness 32344 tailfb 32372 ontopbas 32427 neificl 33549 metf1o 33551 crngohomfo 33805 smprngopr 33851 ispridlc 33869 prter2 34166 snatpsubN 35036 pclclN 35177 pclfinN 35186 ltrncnv 35432 cdleme24 35640 cdleme28 35661 cdleme50ltrn 35845 cdleme 35848 ltrnco 36007 cdlemk28-3 36196 diaf11N 36338 dibf11N 36450 dihlsscpre 36523 mapdpg 36995 mapdh9a 37079 mapdh9aOLDN 37080 hdmap14lem6 37165 mzpincl 37297 mzpindd 37309 iunconnlem2 39171 islptre 39851 lmod1 42281 |
Copyright terms: Public domain | W3C validator |