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 2145   ⊆ wss 3899  {cpr 4586

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-sn 4585  df-pr 4587

This theorem is used by:  prssd  4783  tpssi  4798  fr2nr  5628  fprb  7199  f1ofvswap  7314  ordunel  7838  rex2dom  9244  dfac2b  10209  tskpr  10855  pr01ssre  11312  m1expcl2  14228  m1expcl  14229  wrdlen2i  15093  gcdcllem3  16671  lcmfpr  16802  mreincl  17769  acsfn2  17837  ipole  18708  pmtr3ncom  19689  subrngin  20813  subrgin  20848  lssincl  21240  lspvadd  21371  cnmsgnbas  21884  cnmsgngrp  21885  psgninv  21888  zrhpsgnmhm  21890  mdetunilem7  22933  unopn  23221  incld  23361  indiscld  23409  leordtval2  23530  ovolioo  25889  i1f1  26011  aannenlem2  26656  upgrbi  29671  umgrbi  29679  frgr3vlem2  30875  4cycl2v2nb  30890  sshjval3  31956  psgnid  33658  pmtrto1cl  33660  cnmsgn0g  33707  altgnsg  33710  inlidl  33971  constrsscn  34372  constrextdg2  34381  mdetpmtr1  34455  mdetpmtr12  34457  esumsnf  34696  prsiga  34763  measssd  34848  carsgsigalem  34947  carsgclctun  34953  pmeasmono  34956  eulerpartlemgs2  35012  eulerpartlemn  35013  probun  35051  signswch  35190  signsvfn  35211  signlem0  35216  breprexpnat  35263  kur14lem1  35971  ssoninhaus  37236  poimirlem15  38553  impprop  38644  inidl  38964  pmapmeet  40830  diameetN  42113  dihmeetcN  42359  dihmeet  42400  dvh4dimlem  42500  dvhdimlem  42501  dvh4dimN  42504  dvh3dim3N  42506  lcfrlem23  42622  lcfrlem25  42624  lcfrlem35  42634  mapdindp2  42778  lspindp5  42827  brfvrcld  44690  corclrcl  44706  corcltrcl  44738  ibliooicc  46980  fourierdlem51  47166  fourierdlem64  47179  fourierdlem102  47217  fourierdlem114  47229  sge0sn  47388  ovnsubadd2lem  47654  sprvalpw  48561  prprvalpw  48596  perfectALTVlem2  48819  nnsum3primesgbe  48889  clnbgredg  48937  uhgrimprop  48989  isuspgrimlem  48992  isubgr3stgrlem7  49069  usgrexmpl1lem  49118  usgrexmpl2lem  49123  usgrexmpl2nb1  49129  usgrexmpl2nb2  49130  usgrexmpl2nb4  49132  usgrexmpl2nb5  49133  pgnbgreunbgr  49222  fprmappr  49456  zlmodzxzel  49466  zlmodzxzldeplem1  49611  2arymaptfo  49765  prelrrx2  49824  line2x  49865  line2y  49866  onsetreclem2  50798