Theorem prssi 4765

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

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

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 3432  df-un 3895  df-ss 3907  df-sn 4569  df-pr 4571

This theorem is referenced by:  prssd  4766  tpssi  4782  fr2nr  5602  fprb  7143  f1ofvswap  7255  ordunel  7772  rex2dom  9157  dfac2b  10047  tskpr  10687  pr01ssre  11142  m1expcl2  14041  m1expcl  14042  wrdlen2i  14898  gcdcllem3  16464  lcmfpr  16590  mreincl  17555  acsfn2  17623  ipole  18494  pmtr3ncom  19444  subrngin  20532  subrgin  20567  lssincl  20954  lspvadd  21086  cnmsgnbas  21571  cnmsgngrp  21572  psgninv  21575  zrhpsgnmhm  21577  mdetunilem7  22596  unopn  22881  incld  23021  indiscld  23069  leordtval2  23190  ovolioo  25548  i1f1  25670  aannenlem2  26309  upgrbi  29179  umgrbi  29187  frgr3vlem2  30362  4cycl2v2nb  30377  sshjval3  31443  psgnid  33176  pmtrto1cl  33178  cnmsgn0g  33225  altgnsg  33228  constrsscn  33903  constrextdg2  33912  mdetpmtr1  33986  mdetpmtr12  33988  esumsnf  34227  prsiga  34294  difelsiga  34296  measssd  34378  carsgsigalem  34478  carsgclctun  34484  pmeasmono  34487  eulerpartlemgs2  34543  eulerpartlemn  34544  probun  34582  signswch  34724  signsvfn  34745  signlem0  34750  breprexpnat  34797  kur14lem1  35407  ssoninhaus  36649  poimirlem15  37973  inidl  38368  pmapmeet  40236  diameetN  41519  dihmeetcN  41765  dihmeet  41806  dvh4dimlem  41906  dvhdimlem  41907  dvh4dimN  41910  dvh3dim3N  41912  lcfrlem23  42028  lcfrlem25  42030  lcfrlem35  42040  mapdindp2  42184  lspindp5  42233  brfvrcld  44139  corclrcl  44155  corcltrcl  44187  ibliooicc  46420  fourierdlem51  46606  fourierdlem64  46619  fourierdlem102  46657  fourierdlem114  46669  sge0sn  46828  ovnsubadd2lem  47094  sprvalpw  47955  prprvalpw  47990  perfectALTVlem2  48213  nnsum3primesgbe  48283  clnbgredg  48331  uhgrimprop  48383  isuspgrimlem  48386  isubgr3stgrlem7  48463  usgrexmpl1lem  48512  usgrexmpl2lem  48517  usgrexmpl2nb1  48523  usgrexmpl2nb2  48524  usgrexmpl2nb4  48526  usgrexmpl2nb5  48527  pgnbgreunbgr  48616  fprmappr  48836  zlmodzxzel  48846  zlmodzxzldeplem1  48991  2arymaptfo  49145  prelrrx2  49204  line2x  49245  line2y  49246  onsetreclem2  50196