Theorem prssi 4787

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143   ⊆ wss 3905  {cpr 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-ss 3922  df-sn 4590  df-pr 4592

This theorem is referenced by:  prssd  4788  tpssi  4803  fr2nr  5638  fprb  7192  f1ofvswap  7304  ordunel  7819  rex2dom  9209  dfac2b  10110  tskpr  10750  pr01ssre  11207  m1expcl2  14117  m1expcl  14118  wrdlen2i  14975  gcdcllem3  16554  lcmfpr  16680  mreincl  17646  acsfn2  17714  ipole  18585  pmtr3ncom  19540  subrngin  20660  subrgin  20695  lssincl  21086  lspvadd  21217  cnmsgnbas  21728  cnmsgngrp  21729  psgninv  21732  zrhpsgnmhm  21734  mdetunilem7  22775  unopn  23060  incld  23200  indiscld  23248  leordtval2  23369  ovolioo  25727  i1f1  25849  aannenlem2  26492  upgrbi  29443  umgrbi  29451  frgr3vlem2  30625  4cycl2v2nb  30640  sshjval3  31706  psgnid  33417  pmtrto1cl  33419  cnmsgn0g  33466  altgnsg  33469  inlidl  33729  constrsscn  34130  constrextdg2  34139  mdetpmtr1  34213  mdetpmtr12  34215  esumsnf  34454  prsiga  34521  difelsiga  34523  measssd  34605  carsgsigalem  34705  carsgclctun  34711  pmeasmono  34714  eulerpartlemgs2  34770  eulerpartlemn  34771  probun  34809  signswch  34948  signsvfn  34969  signlem0  34974  breprexpnat  35021  kur14lem1  35698  ssoninhaus  36979  poimirlem15  38306  inidl  38701  pmapmeet  40567  diameetN  41850  dihmeetcN  42096  dihmeet  42137  dvh4dimlem  42237  dvhdimlem  42238  dvh4dimN  42241  dvh3dim3N  42243  lcfrlem23  42359  lcfrlem25  42361  lcfrlem35  42371  mapdindp2  42515  lspindp5  42564  brfvrcld  44437  corclrcl  44453  corcltrcl  44485  ibliooicc  46705  fourierdlem51  46891  fourierdlem64  46904  fourierdlem102  46942  fourierdlem114  46954  sge0sn  47113  ovnsubadd2lem  47379  sprvalpw  48249  prprvalpw  48284  perfectALTVlem2  48507  nnsum3primesgbe  48577  clnbgredg  48625  uhgrimprop  48677  isuspgrimlem  48680  isubgr3stgrlem7  48757  usgrexmpl1lem  48806  usgrexmpl2lem  48811  usgrexmpl2nb1  48817  usgrexmpl2nb2  48818  usgrexmpl2nb4  48820  usgrexmpl2nb5  48821  pgnbgreunbgr  48910  fprmappr  49145  zlmodzxzel  49155  zlmodzxzldeplem1  49300  2arymaptfo  49454  prelrrx2  49513  line2x  49554  line2y  49555  onsetreclem2  50504