![]() |
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 4581 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)) | |
2 | 1 | ibi 259 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∈ wcel 2107 ⊆ wss 3792 {cpr 4400 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-v 3400 df-un 3797 df-in 3799 df-ss 3806 df-sn 4399 df-pr 4401 |
This theorem is referenced by: prssd 4584 tpssi 4598 fr2nr 5333 fprb 6731 ordunel 7305 1sdom 8451 dfac2b 9286 dfac2OLD 9288 tskpr 9927 m1expcl2 13200 m1expcl 13201 wrdlen2i 14093 gcdcllem3 15629 lcmfpr 15746 mreincl 16645 acsfn2 16709 ipole 17544 pmtr3ncom 18278 subrgin 19195 lssincl 19360 lspprcl 19373 lsptpcl 19374 lspprid1 19392 lspvadd 19491 lsppratlem2 19545 lsppratlem4 19547 cnmsgnbas 20319 cnmsgngrp 20320 psgninv 20323 zrhpsgnmhm 20325 mdetralt 20819 mdetunilem7 20829 unopn 21115 pptbas 21220 incld 21255 indiscld 21303 leordtval2 21424 isconn2 21626 xpsdsval 22594 ovolioo 23772 i1f1 23894 itgioo 24019 aannenlem2 24521 wilthlem2 25247 perfectlem2 25407 upgrbi 26441 umgrbi 26449 frgr3vlem2 27682 4cycl2v2nb 27697 sshjval3 28785 pr01ssre 30134 psgnid 30445 pmtrto1cl 30447 mdetpmtr1 30487 mdetpmtr12 30489 esumsnf 30724 prsiga 30792 difelsiga 30794 inelpisys 30815 measssd 30876 carsgsigalem 30975 carsgclctun 30981 pmeasmono 30984 eulerpartlemgs2 31040 eulerpartlemn 31041 probun 31080 signswch 31238 signsvfn 31261 signlem0 31266 breprexpnat 31314 kur14lem1 31787 ssoninhaus 33030 lindsadd 34030 poimirlem15 34052 inidl 34455 pmapmeet 35929 diameetN 37212 dihmeetcN 37458 dihmeet 37499 dvh4dimlem 37599 dvhdimlem 37600 dvh4dimN 37603 dvh3dim3N 37605 lcfrlem23 37721 lcfrlem25 37723 lcfrlem35 37733 mapdindp2 37877 lspindp5 37926 brfvrcld 38944 corclrcl 38960 corcltrcl 38992 ibliooicc 41118 fourierdlem51 41305 fourierdlem64 41318 fourierdlem102 41356 fourierdlem114 41368 sge0sn 41524 ovnsubadd2lem 41790 sprvalpw 42423 prprvalpw 42458 perfectALTVlem2 42660 nnsum3primesgbe 42709 mapprop 43143 zlmodzxzel 43152 zlmodzxzldeplem1 43308 prelrrx2 43453 line2x 43494 line2y 43495 onsetreclem2 43561 |
Copyright terms: Public domain | W3C validator |