Theorem prssi 4826

Description: A pair of elements of a class is a subset of the class. (Contributed by NM, 16-Jan-2015.)

Assertion

Ref	Expression
prssi	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶)

Proof of Theorem prssi

Step	Hyp	Ref	Expression
1		prssg 4824	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶))
2	1	ibi 266	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶)

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