Theorem prssi 4782

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147   ⊆ wss 3900  {cpr 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  prssd  4783  tpssi  4798  fr2nr  5635  fprb  7230  f1ofvswap  7345  ordunel  7872  rex2dom  9282  dfac2b  10248  tskpr  10894  pr01ssre  11351  m1expcl2  14268  m1expcl  14269  wrdlen2i  15136  gcdcllem3  16715  lcmfpr  16846  mreincl  17819  acsfn2  17887  ipole  18758  pmtr3ncom  19740  subrngin  20864  subrgin  20899  lssincl  21291  lspvadd  21422  cnmsgnbas  21939  cnmsgngrp  21940  psgninv  21943  zrhpsgnmhm  21945  mdetunilem7  22988  unopn  23276  incld  23416  indiscld  23464  leordtval2  23585  ovolioo  25944  i1f1  26066  aannenlem2  26713  upgrbi  29728  umgrbi  29736  frgr3vlem2  30932  4cycl2v2nb  30947  sshjval3  32013  psgnid  33757  pmtrto1cl  33759  cnmsgn0g  33806  altgnsg  33809  inlidl  34075  constrsscn  34483  constrextdg2  34492  mdetpmtr1  34566  mdetpmtr12  34568  esumsnf  34807  prsiga  34874  measssd  34959  carsgsigalem  35058  carsgclctun  35064  pmeasmono  35067  eulerpartlemgs2  35123  eulerpartlemn  35124  probun  35162  signswch  35301  signsvfn  35322  signlem0  35327  breprexpnat  35374  kur14lem1  36179  ssoninhaus  37451  poimirlem15  38821  impprop  38912  inidl  39230  pmapmeet  41096  diameetN  42379  dihmeetcN  42625  dihmeet  42666  dvh4dimlem  42766  dvhdimlem  42767  dvh4dimN  42770  dvh3dim3N  42772  lcfrlem23  42888  lcfrlem25  42890  lcfrlem35  42900  mapdindp2  43044  lspindp5  43093  brfvrcld  44952  corclrcl  44968  corcltrcl  45000  ibliooicc  47254  fourierdlem51  47440  fourierdlem64  47453  fourierdlem102  47491  fourierdlem114  47503  sge0sn  47662  ovnsubadd2lem  47928  sprvalpw  48835  prprvalpw  48870  perfectALTVlem2  49093  nnsum3primesgbe  49163  clnbgredg  49211  uhgrimprop  49263  isuspgrimlem  49266  isubgr3stgrlem7  49343  usgrexmpl1lem  49392  usgrexmpl2lem  49397  usgrexmpl2nb1  49403  usgrexmpl2nb2  49404  usgrexmpl2nb4  49406  usgrexmpl2nb5  49407  pgnbgreunbgr  49496  fprmappr  49788  zlmodzxzel  49798  zlmodzxzldeplem1  49943  2arymaptfo  50097  onsetreclem2  51205