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 3562 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | anim1d 586 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑))) |
3 | 2 | reximdv2 2997 | 1 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1977 ∃wrex 2897 ⊆ wss 3540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-rex 2902 df-in 3547 df-ss 3554 |
This theorem is referenced by: iunss1 4468 onfr 5680 moriotass 6539 frxp 7174 frfi 8090 fisupcl 8258 supgtoreq 8259 brwdom3 8370 unwdomg 8372 tcrank 8630 hsmexlem2 9132 pwfseqlem3 9361 grur1 9521 suplem1pr 9753 fimaxre2 10848 suprfinzcl 11368 lbzbi 11652 suprzub 11655 uzsupss 11656 zmin 11660 ssnn0fi 12646 elss2prb 13123 scshwfzeqfzo 13423 rexico 13941 rlim3 14077 rlimclim 14125 caurcvgr 14252 alzdvds 14880 bitsfzolem 14994 pclem 15381 0ram2 15563 0ramcl 15565 symgextfo 17665 lsmless1x 17882 lsmless2x 17883 dprdss 18251 ablfac2 18311 subrgdvds 18617 ssrest 20790 locfincf 21144 fbun 21454 fgss 21487 isucn2 21893 metust 22173 psmetutop 22182 lebnumlem3 22570 lebnum 22571 cfil3i 22875 cfilss 22876 fgcfil 22877 iscau4 22885 ivthle 23032 ivthle2 23033 lhop1lem 23580 lhop2 23582 ply1divex 23700 plyss 23759 dgrlem 23789 elqaa 23881 aannenlem2 23888 reeff1olem 24004 rlimcnp 24492 ftalem3 24601 pntlem3 25098 tgisline 25322 axcontlem2 25645 frgrawopreg1 26577 frgrawopreg2 26578 shless 27602 xlt2addrd 28913 ssnnssfz 28937 xreceu 28961 archirngz 29074 archiabllem1b 29077 locfinreflem 29235 crefss 29244 esumpcvgval 29467 sigaclci 29522 eulerpartlemgvv 29765 eulerpartlemgh 29767 signsply0 29954 iccllyscon 30486 frmin 30983 nodenselem4 31083 fgmin 31535 knoppndvlem18 31690 poimirlem26 32605 poimirlem30 32609 volsupnfl 32624 cover2 32678 filbcmb 32705 istotbnd3 32740 sstotbnd 32744 heibor1lem 32778 isdrngo2 32927 isdrngo3 32928 islsati 33299 paddss1 34121 paddss2 34122 hdmap14lem2a 36177 pellfundre 36463 pellfundge 36464 pellfundglb 36467 hbtlem3 36716 hbtlem5 36717 itgoss 36752 radcnvrat 37535 fiminre2 38535 climleltrp 38743 fourierdlem20 39020 smflimlem2 39658 iccelpart 39971 fmtnofac2 40019 ssn0rex 40311 frgrwopreg1 41487 frgrwopreg2 41488 ssnn0ssfz 41920 pgrpgt2nabl 41941 |
Copyright terms: Public domain | W3C validator |