| 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.) Avoid axioms. (Revised by GG, 19-May-2025.) |
| Ref | Expression |
|---|---|
| ssrexv | ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ss 3925 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
| 2 | pm3.45 634 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑))) | |
| 3 | 2 | aleximi 1865 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))) |
| 4 | df-rex 3093 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
| 5 | df-rex 3093 | . . 3 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)) | |
| 6 | 3, 4, 5 | 3imtr4g 299 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑)) |
| 7 | 1, 6 | sylbi 220 | 1 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑)) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∀wal 1568 ∃wex 1812 ∈ wcel 2146 ∃wrex 3092 ⊆ wss 3908 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 |
| This proof depends on definitions: df-bi 210 df-an 402 df-ex 1813 df-rex 3093 df-ss 3925 |
| This theorem is used by: ss2rexv 4012 ssn0rex 4316 iunss1 4976 onfr 6407 moriotass 7412 frxp 8131 frfi 9255 fisupcl 9440 supgtoreq 9441 brwdom3 9554 unwdomg 9556 frmin 9731 tcrank 9866 hsmexlem2 10429 pwfseqlem3 10663 grur1 10823 suplem1pr 11055 fimaxre2 12178 fiminre2 12181 suprfinzcl 12728 lbzbi 12978 suprzub 12981 uzsupss 12982 zmin 12986 ssnn0fi 14041 elss2prb 14545 scshwfzeqfzo 14889 rexico 15431 rlim3 15575 rlimclim 15623 caurcvgr 15751 alzdvds 16403 bitsfzolem 16517 pclem 16923 0ram2 17106 0ramcl 17108 symgextfo 19523 lsmless1x 19745 lsmless2x 19746 dprdss 20132 ablfac2 20192 subrgdvds 20722 isdrng3lem2 20889 isdrng5 20891 ssrest 23370 locfincf 23725 fbun 24034 fgss 24067 isucn2 24472 metust 24752 psmetutop 24761 lebnumlem3 25159 lebnum 25160 cfil3i 25465 cfilss 25466 fgcfil 25467 iscau4 25475 ivthle 25652 ivthle2 25653 lhop1lem 26209 lhop2 26211 ply1divex 26331 plyss 26393 dgrlem 26423 elqaa 26520 aannenlem2 26529 reeff1olem 26646 rlimcnp 27167 ftalem3 27276 2sqreultblem 27649 2sqreunnlem1 27650 2sqreunnltblem 27652 pntlem3 27810 madess 28096 addsuniflem 28231 mulsuniflem 28379 tgisline 28937 axcontlem2 29352 frgrwopreg1 30706 frgrwopreg2 30707 shless 31748 xlt2addrd 33141 ssnnssfz 33169 xreceu 33278 archirngz 33540 archiabllem1b 33543 1arithidom 33858 dfufd2lem 33870 locfinreflem 34261 crefss 34270 esumpcvgval 34499 sigaclci 34553 eulerpartlemgvv 34797 eulerpartlemgh 34799 signsply0 34969 iccllysconn 35762 satfvsucsuc 35877 fgmin 36921 knoppndvlem18 37158 poimirlem26 38337 poimirlem30 38341 volsupnfl 38356 cover2 38406 filbcmb 38431 istotbnd3 38462 sstotbnd 38466 heibor1lem 38500 isdrngo2 38649 isdrngo3 38650 qsss1 38984 islsati 39808 paddss1 40631 paddss2 40632 hdmap14lem2a 42681 prjspreln0 43381 pellfundre 43648 pellfundge 43649 pellfundglb 43652 hbtlem3 43894 hbtlem5 43895 itgoss 43930 radcnvrat 45064 uzubico 46322 uzubico2 46324 climleltrp 46430 fourierdlem20 46881 smflimlem2 47526 nndivides2 48161 iccelpart 48222 fmtnofac2 48361 grtriprop 48746 ssnn0ssfz 49169 pgrpgt2nabl 49186 eenglngeehlnmlem1 49557 |
| Copyright terms: Public domain | W3C validator |