![]() |
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 3630 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | anim1d 587 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑))) |
3 | 2 | reximdv2 3043 | 1 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2030 ∃wrex 2942 ⊆ wss 3607 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-rex 2947 df-in 3614 df-ss 3621 |
This theorem is referenced by: ssn0rex 3969 iunss1 4564 onfr 5801 moriotass 6680 frxp 7332 frfi 8246 fisupcl 8416 supgtoreq 8417 brwdom3 8528 unwdomg 8530 tcrank 8785 hsmexlem2 9287 pwfseqlem3 9520 grur1 9680 suplem1pr 9912 fimaxre2 11007 suprfinzcl 11530 lbzbi 11814 suprzub 11817 uzsupss 11818 zmin 11822 ssnn0fi 12824 elss2prb 13307 scshwfzeqfzo 13618 rexico 14137 rlim3 14273 rlimclim 14321 caurcvgr 14448 alzdvds 15089 bitsfzolem 15203 pclem 15590 0ram2 15772 0ramcl 15774 symgextfo 17888 lsmless1x 18105 lsmless2x 18106 dprdss 18474 ablfac2 18534 subrgdvds 18842 ssrest 21028 locfincf 21382 fbun 21691 fgss 21724 isucn2 22130 metust 22410 psmetutop 22419 lebnumlem3 22809 lebnum 22810 cfil3i 23113 cfilss 23114 fgcfil 23115 iscau4 23123 ivthle 23271 ivthle2 23272 lhop1lem 23821 lhop2 23823 ply1divex 23941 plyss 24000 dgrlem 24030 elqaa 24122 aannenlem2 24129 reeff1olem 24245 rlimcnp 24737 ftalem3 24846 pntlem3 25343 tgisline 25567 axcontlem2 25890 frgrwopreg1 27298 frgrwopreg2 27299 shless 28346 xlt2addrd 29651 ssnnssfz 29677 xreceu 29758 archirngz 29871 archiabllem1b 29874 locfinreflem 30035 crefss 30044 esumpcvgval 30268 sigaclci 30323 eulerpartlemgvv 30566 eulerpartlemgh 30568 signsply0 30756 iccllysconn 31358 frmin 31867 fgmin 32490 knoppndvlem18 32645 poimirlem26 33565 poimirlem30 33569 volsupnfl 33584 cover2 33638 filbcmb 33665 istotbnd3 33700 sstotbnd 33704 heibor1lem 33738 isdrngo2 33887 isdrngo3 33888 qsss1 34194 islsati 34599 paddss1 35421 paddss2 35422 hdmap14lem2a 37476 pellfundre 37762 pellfundge 37763 pellfundglb 37766 hbtlem3 38014 hbtlem5 38015 itgoss 38050 radcnvrat 38830 fiminre2 39907 uzubico 40113 uzubico2 40115 climleltrp 40226 fourierdlem20 40662 smflimlem2 41301 iccelpart 41694 fmtnofac2 41806 ssnn0ssfz 42452 pgrpgt2nabl 42472 |
Copyright terms: Public domain | W3C validator |