Theorem prssi 4777

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   ⊆ wss 3901  {cpr 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-sn 4581  df-pr 4583

This theorem is referenced by:  prssd  4778  tpssi  4794  fr2nr  5601  fprb  7140  f1ofvswap  7252  ordunel  7769  rex2dom  9155  dfac2b  10043  tskpr  10683  m1expcl2  14010  m1expcl  14011  wrdlen2i  14867  gcdcllem3  16430  lcmfpr  16556  mreincl  17520  acsfn2  17588  ipole  18459  pmtr3ncom  19406  subrngin  20496  subrgin  20531  lssincl  20918  lspvadd  21050  cnmsgnbas  21535  cnmsgngrp  21536  psgninv  21539  zrhpsgnmhm  21541  mdetunilem7  22564  unopn  22849  incld  22989  indiscld  23037  leordtval2  23158  ovolioo  25527  i1f1  25649  aannenlem2  26295  upgrbi  29168  umgrbi  29176  frgr3vlem2  30351  4cycl2v2nb  30366  sshjval3  31431  pr01ssre  32907  psgnid  33181  pmtrto1cl  33183  cnmsgn0g  33230  altgnsg  33233  constrsscn  33899  constrextdg2  33908  mdetpmtr1  33982  mdetpmtr12  33984  esumsnf  34223  prsiga  34290  difelsiga  34292  measssd  34374  carsgsigalem  34474  carsgclctun  34480  pmeasmono  34483  eulerpartlemgs2  34539  eulerpartlemn  34540  probun  34578  signswch  34720  signsvfn  34741  signlem0  34746  breprexpnat  34793  kur14lem1  35402  ssoninhaus  36644  poimirlem15  37838  inidl  38233  pmapmeet  40055  diameetN  41338  dihmeetcN  41584  dihmeet  41625  dvh4dimlem  41725  dvhdimlem  41726  dvh4dimN  41729  dvh3dim3N  41731  lcfrlem23  41847  lcfrlem25  41849  lcfrlem35  41859  mapdindp2  42003  lspindp5  42052  brfvrcld  43953  corclrcl  43969  corcltrcl  44001  ibliooicc  46236  fourierdlem51  46422  fourierdlem64  46435  fourierdlem102  46473  fourierdlem114  46485  sge0sn  46644  ovnsubadd2lem  46910  sprvalpw  47747  prprvalpw  47782  perfectALTVlem2  47989  nnsum3primesgbe  48059  clnbgredg  48107  uhgrimprop  48159  isuspgrimlem  48162  isubgr3stgrlem7  48239  usgrexmpl1lem  48288  usgrexmpl2lem  48293  usgrexmpl2nb1  48299  usgrexmpl2nb2  48300  usgrexmpl2nb4  48302  usgrexmpl2nb5  48303  pgnbgreunbgr  48392  fprmappr  48612  zlmodzxzel  48622  zlmodzxzldeplem1  48767  2arymaptfo  48921  prelrrx2  48980  line2x  49021  line2y  49022  onsetreclem2  49972