![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > prssi | Structured version Visualization version GIF version |
Description: A pair of elements of a class is a subset of the class. (Contributed by NM, 16-Jan-2015.) |
Ref | Expression |
---|---|
prssi | ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prssg 4824 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)) | |
2 | 1 | ibi 266 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∈ wcel 2098 ⊆ wss 3944 {cpr 4632 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-v 3463 df-un 3949 df-ss 3961 df-sn 4631 df-pr 4633 |
This theorem is referenced by: prssd 4827 tpssi 4841 fr2nr 5656 fprb 7206 f1ofvswap 7314 ordunel 7831 rex2dom 9274 1sdomOLD 9277 dfac2b 10160 tskpr 10800 m1expcl2 14091 m1expcl 14092 wrdlen2i 14934 gcdcllem3 16484 lcmfpr 16606 mreincl 17587 acsfn2 17651 ipole 18534 pmtr3ncom 19447 subrngin 20515 subrgin 20552 lssincl 20866 lspvadd 20998 cnmsgnbas 21532 cnmsgngrp 21533 psgninv 21536 zrhpsgnmhm 21538 mdetunilem7 22569 unopn 22854 incld 22996 indiscld 23044 leordtval2 23165 ovolioo 25546 i1f1 25668 aannenlem2 26314 upgrbi 28983 umgrbi 28991 frgr3vlem2 30161 4cycl2v2nb 30176 sshjval3 31241 pr01ssre 32677 psgnid 32915 pmtrto1cl 32917 cnmsgn0g 32964 altgnsg 32967 mdetpmtr1 33557 mdetpmtr12 33559 esumsnf 33816 prsiga 33883 difelsiga 33885 measssd 33967 carsgsigalem 34068 carsgclctun 34074 pmeasmono 34077 eulerpartlemgs2 34133 eulerpartlemn 34134 probun 34172 signswch 34326 signsvfn 34347 signlem0 34352 breprexpnat 34399 kur14lem1 34949 ssoninhaus 36065 poimirlem15 37241 inidl 37636 pmapmeet 39378 diameetN 40661 dihmeetcN 40907 dihmeet 40948 dvh4dimlem 41048 dvhdimlem 41049 dvh4dimN 41052 dvh3dim3N 41054 lcfrlem23 41170 lcfrlem25 41172 lcfrlem35 41182 mapdindp2 41326 lspindp5 41375 brfvrcld 43265 corclrcl 43281 corcltrcl 43313 ibliooicc 45499 fourierdlem51 45685 fourierdlem64 45698 fourierdlem102 45736 fourierdlem114 45748 sge0sn 45907 ovnsubadd2lem 46173 sprvalpw 46959 prprvalpw 46994 perfectALTVlem2 47201 nnsum3primesgbe 47271 uspgrimprop 47359 isuspgrimlem 47360 fprmappr 47597 zlmodzxzel 47607 zlmodzxzldeplem1 47756 2arymaptfo 47915 prelrrx2 47974 line2x 48015 line2y 48016 onsetreclem2 48325 |
Copyright terms: Public domain | W3C validator |