![]() |
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 3940 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | anim1d 611 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑))) |
3 | 2 | reximdv2 3157 | 1 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 ∃wrex 3069 ⊆ wss 3913 |
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 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-rex 3070 df-v 3448 df-in 3920 df-ss 3930 |
This theorem is referenced by: ss2rexv 4018 ssn0rex 4320 iunss1 4973 onfr 6361 moriotass 7351 frxp 8063 frfi 9239 fisupcl 9414 supgtoreq 9415 brwdom3 9527 unwdomg 9529 frmin 9694 tcrank 9829 hsmexlem2 10372 pwfseqlem3 10605 grur1 10765 suplem1pr 10997 fimaxre2 12109 fiminre2 12112 suprfinzcl 12626 lbzbi 12870 suprzub 12873 uzsupss 12874 zmin 12878 ssnn0fi 13900 elss2prb 14398 scshwfzeqfzo 14727 rexico 15250 rlim3 15392 rlimclim 15440 caurcvgr 15570 alzdvds 16213 bitsfzolem 16325 pclem 16721 0ram2 16904 0ramcl 16906 symgextfo 19218 lsmless1x 19440 lsmless2x 19441 dprdss 19822 ablfac2 19882 subrgdvds 20284 ssrest 22564 locfincf 22919 fbun 23228 fgss 23261 isucn2 23668 metust 23951 psmetutop 23960 lebnumlem3 24363 lebnum 24364 cfil3i 24670 cfilss 24671 fgcfil 24672 iscau4 24680 ivthle 24857 ivthle2 24858 lhop1lem 25414 lhop2 25416 ply1divex 25538 plyss 25597 dgrlem 25627 elqaa 25719 aannenlem2 25726 reeff1olem 25842 rlimcnp 26352 ftalem3 26461 2sqreultblem 26833 2sqreunnlem1 26834 2sqreunnltblem 26836 pntlem3 26994 madess 27249 addsunif 27353 tgisline 27632 axcontlem2 27977 frgrwopreg1 29325 frgrwopreg2 29326 shless 30364 xlt2addrd 31731 ssnnssfz 31758 xreceu 31848 archirngz 32095 archiabllem1b 32098 locfinreflem 32510 crefss 32519 esumpcvgval 32766 sigaclci 32820 eulerpartlemgvv 33065 eulerpartlemgh 33067 signsply0 33252 iccllysconn 33931 satfvsucsuc 34046 fgmin 34918 knoppndvlem18 35068 poimirlem26 36177 poimirlem30 36181 volsupnfl 36196 cover2 36246 filbcmb 36272 istotbnd3 36303 sstotbnd 36307 heibor1lem 36341 isdrngo2 36490 isdrngo3 36491 qsss1 36822 islsati 37529 paddss1 38353 paddss2 38354 hdmap14lem2a 40403 prjspreln0 41005 pellfundre 41262 pellfundge 41263 pellfundglb 41266 hbtlem3 41512 hbtlem5 41513 itgoss 41548 radcnvrat 42716 uzubico 43926 uzubico2 43928 climleltrp 44037 fourierdlem20 44488 smflimlem2 45133 iccelpart 45745 fmtnofac2 45881 ssnn0ssfz 46545 pgrpgt2nabl 46562 eenglngeehlnmlem1 46943 |
Copyright terms: Public domain | W3C validator |