![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssrexv | Structured version Visualization version GIF version |
Description: Existential quantification restricted to a subclass. (Contributed by NM, 11-Jan-2007.) |
Ref | Expression |
---|---|
ssrexv | ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3937 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | anim1d 611 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑))) |
3 | 2 | reximdv2 3161 | 1 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 ∃wrex 3073 ⊆ wss 3910 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-rex 3074 df-v 3447 df-in 3917 df-ss 3927 |
This theorem is referenced by: ss2rexv 4013 ssn0rex 4315 iunss1 4968 onfr 6356 moriotass 7346 frxp 8058 frfi 9232 fisupcl 9405 supgtoreq 9406 brwdom3 9518 unwdomg 9520 frmin 9685 tcrank 9820 hsmexlem2 10363 pwfseqlem3 10596 grur1 10756 suplem1pr 10988 fimaxre2 12100 fiminre2 12103 suprfinzcl 12617 lbzbi 12861 suprzub 12864 uzsupss 12865 zmin 12869 ssnn0fi 13890 elss2prb 14386 scshwfzeqfzo 14715 rexico 15238 rlim3 15380 rlimclim 15428 caurcvgr 15558 alzdvds 16202 bitsfzolem 16314 pclem 16710 0ram2 16893 0ramcl 16895 symgextfo 19204 lsmless1x 19426 lsmless2x 19427 dprdss 19808 ablfac2 19868 subrgdvds 20236 ssrest 22527 locfincf 22882 fbun 23191 fgss 23224 isucn2 23631 metust 23914 psmetutop 23923 lebnumlem3 24326 lebnum 24327 cfil3i 24633 cfilss 24634 fgcfil 24635 iscau4 24643 ivthle 24820 ivthle2 24821 lhop1lem 25377 lhop2 25379 ply1divex 25501 plyss 25560 dgrlem 25590 elqaa 25682 aannenlem2 25689 reeff1olem 25805 rlimcnp 26315 ftalem3 26424 2sqreultblem 26796 2sqreunnlem1 26797 2sqreunnltblem 26799 pntlem3 26957 madess 27206 addsunif 27310 tgisline 27569 axcontlem2 27914 frgrwopreg1 29262 frgrwopreg2 29263 shless 30301 xlt2addrd 31663 ssnnssfz 31690 xreceu 31778 archirngz 32025 archiabllem1b 32028 locfinreflem 32421 crefss 32430 esumpcvgval 32677 sigaclci 32731 eulerpartlemgvv 32976 eulerpartlemgh 32978 signsply0 33163 iccllysconn 33844 satfvsucsuc 33959 fgmin 34842 knoppndvlem18 34992 poimirlem26 36104 poimirlem30 36108 volsupnfl 36123 cover2 36173 filbcmb 36199 istotbnd3 36230 sstotbnd 36234 heibor1lem 36268 isdrngo2 36417 isdrngo3 36418 qsss1 36749 islsati 37456 paddss1 38280 paddss2 38281 hdmap14lem2a 40330 prjspreln0 40933 pellfundre 41190 pellfundge 41191 pellfundglb 41194 hbtlem3 41440 hbtlem5 41441 itgoss 41476 radcnvrat 42584 uzubico 43796 uzubico2 43798 climleltrp 43907 fourierdlem20 44358 smflimlem2 45003 iccelpart 45615 fmtnofac2 45751 ssnn0ssfz 46415 pgrpgt2nabl 46432 eenglngeehlnmlem1 46813 |
Copyright terms: Public domain | W3C validator |