Theorem prssi 4797

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 4795	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶))
2	1	ibi 267	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ⊆ wss 3926  {cpr 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943  df-sn 4602  df-pr 4604

This theorem is referenced by:  prssd  4798  tpssi  4814  fr2nr  5631  fprb  7186  f1ofvswap  7299  ordunel  7821  rex2dom  9254  1sdomOLD  9257  dfac2b  10145  tskpr  10784  m1expcl2  14103  m1expcl  14104  wrdlen2i  14961  gcdcllem3  16520  lcmfpr  16646  mreincl  17611  acsfn2  17675  ipole  18544  pmtr3ncom  19456  subrngin  20521  subrgin  20556  lssincl  20922  lspvadd  21054  cnmsgnbas  21538  cnmsgngrp  21539  psgninv  21542  zrhpsgnmhm  21544  mdetunilem7  22556  unopn  22841  incld  22981  indiscld  23029  leordtval2  23150  ovolioo  25521  i1f1  25643  aannenlem2  26289  upgrbi  29072  umgrbi  29080  frgr3vlem2  30255  4cycl2v2nb  30270  sshjval3  31335  pr01ssre  32803  psgnid  33108  pmtrto1cl  33110  cnmsgn0g  33157  altgnsg  33160  constrsscn  33774  constrextdg2  33783  mdetpmtr1  33854  mdetpmtr12  33856  esumsnf  34095  prsiga  34162  difelsiga  34164  measssd  34246  carsgsigalem  34347  carsgclctun  34353  pmeasmono  34356  eulerpartlemgs2  34412  eulerpartlemn  34413  probun  34451  signswch  34593  signsvfn  34614  signlem0  34619  breprexpnat  34666  kur14lem1  35228  ssoninhaus  36466  poimirlem15  37659  inidl  38054  pmapmeet  39792  diameetN  41075  dihmeetcN  41321  dihmeet  41362  dvh4dimlem  41462  dvhdimlem  41463  dvh4dimN  41466  dvh3dim3N  41468  lcfrlem23  41584  lcfrlem25  41586  lcfrlem35  41596  mapdindp2  41740  lspindp5  41789  brfvrcld  43715  corclrcl  43731  corcltrcl  43763  ibliooicc  46000  fourierdlem51  46186  fourierdlem64  46199  fourierdlem102  46237  fourierdlem114  46249  sge0sn  46408  ovnsubadd2lem  46674  sprvalpw  47494  prprvalpw  47529  perfectALTVlem2  47736  nnsum3primesgbe  47806  clnbgredg  47853  uhgrimprop  47905  isuspgrimlem  47908  isubgr3stgrlem7  47984  usgrexmpl1lem  48025  usgrexmpl2lem  48030  usgrexmpl2nb1  48036  usgrexmpl2nb2  48037  usgrexmpl2nb4  48039  usgrexmpl2nb5  48040  fprmappr  48320  zlmodzxzel  48330  zlmodzxzldeplem1  48476  2arymaptfo  48634  prelrrx2  48693  line2x  48734  line2y  48735  onsetreclem2  49570