Theorem prssi 4779

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3903  {cpr 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-sn 4583  df-pr 4585

This theorem is referenced by:  prssd  4780  tpssi  4796  fr2nr  5609  fprb  7150  f1ofvswap  7262  ordunel  7779  rex2dom  9165  dfac2b  10053  tskpr  10693  m1expcl2  14020  m1expcl  14021  wrdlen2i  14877  gcdcllem3  16440  lcmfpr  16566  mreincl  17530  acsfn2  17598  ipole  18469  pmtr3ncom  19419  subrngin  20509  subrgin  20544  lssincl  20931  lspvadd  21063  cnmsgnbas  21548  cnmsgngrp  21549  psgninv  21552  zrhpsgnmhm  21554  mdetunilem7  22577  unopn  22862  incld  23002  indiscld  23050  leordtval2  23171  ovolioo  25540  i1f1  25662  aannenlem2  26308  upgrbi  29182  umgrbi  29190  frgr3vlem2  30365  4cycl2v2nb  30380  sshjval3  31446  pr01ssre  32920  psgnid  33195  pmtrto1cl  33197  cnmsgn0g  33244  altgnsg  33247  constrsscn  33922  constrextdg2  33931  mdetpmtr1  34005  mdetpmtr12  34007  esumsnf  34246  prsiga  34313  difelsiga  34315  measssd  34397  carsgsigalem  34497  carsgclctun  34503  pmeasmono  34506  eulerpartlemgs2  34562  eulerpartlemn  34563  probun  34601  signswch  34743  signsvfn  34764  signlem0  34769  breprexpnat  34816  kur14lem1  35426  ssoninhaus  36668  poimirlem15  37890  inidl  38285  pmapmeet  40153  diameetN  41436  dihmeetcN  41682  dihmeet  41723  dvh4dimlem  41823  dvhdimlem  41824  dvh4dimN  41827  dvh3dim3N  41829  lcfrlem23  41945  lcfrlem25  41947  lcfrlem35  41957  mapdindp2  42101  lspindp5  42150  brfvrcld  44051  corclrcl  44067  corcltrcl  44099  ibliooicc  46333  fourierdlem51  46519  fourierdlem64  46532  fourierdlem102  46570  fourierdlem114  46582  sge0sn  46741  ovnsubadd2lem  47007  sprvalpw  47844  prprvalpw  47879  perfectALTVlem2  48086  nnsum3primesgbe  48156  clnbgredg  48204  uhgrimprop  48256  isuspgrimlem  48259  isubgr3stgrlem7  48336  usgrexmpl1lem  48385  usgrexmpl2lem  48390  usgrexmpl2nb1  48396  usgrexmpl2nb2  48397  usgrexmpl2nb4  48399  usgrexmpl2nb5  48400  pgnbgreunbgr  48489  fprmappr  48709  zlmodzxzel  48719  zlmodzxzldeplem1  48864  2arymaptfo  49018  prelrrx2  49077  line2x  49118  line2y  49119  onsetreclem2  50069