![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssralv | Structured version Visualization version GIF version |
Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.) |
Ref | Expression |
---|---|
ssralv | ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3889 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | imim1d 82 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑))) |
3 | 2 | ralimdv2 3145 | 1 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2083 ∀wral 3107 ⊆ wss 3865 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-ext 2771 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-clab 2778 df-cleq 2790 df-clel 2865 df-ral 3112 df-in 3872 df-ss 3880 |
This theorem is referenced by: ss2ralv 3962 intss 4809 iinss1 4845 disjiun 4956 poss 5371 sess2 5419 isores3 6958 isoini2 6962 smores 7848 smores2 7850 tfrlem5 7875 resixp 8352 ac6sfi 8615 iunfi 8665 ixpfi2 8675 marypha1lem 8750 ordtypelem2 8836 tcrank 9166 acndom 9330 pwsdompw 9479 ssfin3ds 9605 fin1a2s 9689 hsmexlem4 9704 domtriomlem 9717 zornn0g 9780 fpwwe2lem13 9917 ingru 10090 cshw1 14024 rexanuz 14543 cau3lem 14552 caubnd 14556 limsupgord 14667 limsupval2 14675 rlimres 14753 lo1res 14754 o1of2 14807 o1rlimmul 14813 climsup 14864 fsumiun 15013 lcmfunsnlem1 15814 coprmprod 15838 pcfac 16068 vdwnnlem2 16165 firest 16539 imasaddfnlem 16634 imasvscafn 16643 psss 17657 tsrss 17666 cntz2ss 18208 cntzmhm2 18215 subgpgp 18456 efgsres 18595 telgsumfzs 18830 telgsums 18834 dprdss 18872 acsfn1p 19272 ocv2ss 20503 mretopd 21388 tgcn 21548 tgcnp 21549 subbascn 21550 cnss2 21573 cncnp 21576 sslm 21595 t1ficld 21623 tgcmp 21697 1stcfb 21741 islly2 21780 dislly 21793 comppfsc 21828 ptbasfi 21877 ptcnplem 21917 tx1stc 21946 qtoptop2 21995 fbunfip 22165 flftg 22292 txflf 22302 fclsbas 22317 fclsss1 22318 fclsss2 22319 alexsubb 22342 tmdgsum2 22392 metrest 22821 rescncf 23192 cnllycmp 23247 bndth 23249 fgcfil 23561 ivthlem2 23740 ivthlem3 23741 ovolsslem 23772 ovolfiniun 23789 finiunmbl 23832 volfiniun 23835 iunmbl 23841 ioombl1lem4 23849 dyadmax 23886 vitali 23901 mbfimaopnlem 23943 mbflimsup 23954 mbfi1flim 24011 ditgeq3 24135 dvferm 24272 rollelem 24273 dvivthlem1 24292 itgsubstlem 24332 aalioulem2 24609 ulmcaulem 24669 ulmss 24672 xrlimcnp 25232 2sqreunnlem2 25717 pntlem3 25871 pntlemp 25872 pntleml 25873 uspgr2wlkeq 27114 redwlk 27140 wwlksm1edg 27345 wwlksnred 27356 clwlkclwwlklem2 27464 clwwlkinwwlk 27504 clwwlkf 27512 wwlksubclwwlk 27523 occon 28751 xrge0infss 30168 resspos 30316 resstos 30317 submarchi 30449 sigaclci 31004 measiun 31090 elmbfmvol2 31138 sibfof 31211 ftc2re 31482 bnj1118 31866 subfacp1lem3 32039 iccllysconn 32107 dmopab3rexdif 32262 untint 32548 untangtr 32550 dfon2lem6 32643 dfon2lem8 32645 dfon2lem9 32646 poseq 32706 soseq 32707 nosepon 32783 noresle 32811 sssslt1 32871 sssslt2 32872 neibastop1 33318 neibastop2lem 33319 neibastop3 33321 finixpnum 34429 ptrecube 34444 poimirlem26 34470 poimirlem27 34471 poimirlem30 34474 heicant 34479 volsupnfl 34489 prdstotbnd 34625 heibor1lem 34640 ispridl2 34869 elrfirn2 38799 rabdiophlem1 38904 dford3lem1 39129 kelac1 39169 ssralv2 40425 ssralv2VD 40760 climinf 41450 limsupvaluz2 41582 supcnvlimsup 41584 iccpartres 43082 |
Copyright terms: Public domain | W3C validator |