Theorem prssi 4775

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

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

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 2706

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 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-ss 3916  df-sn 4579  df-pr 4581

This theorem is referenced by:  prssd  4776  tpssi  4792  fr2nr  5599  fprb  7138  f1ofvswap  7250  ordunel  7767  rex2dom  9151  dfac2b  10039  tskpr  10679  m1expcl2  14006  m1expcl  14007  wrdlen2i  14863  gcdcllem3  16426  lcmfpr  16552  mreincl  17516  acsfn2  17584  ipole  18455  pmtr3ncom  19402  subrngin  20492  subrgin  20527  lssincl  20914  lspvadd  21046  cnmsgnbas  21531  cnmsgngrp  21532  psgninv  21535  zrhpsgnmhm  21537  mdetunilem7  22560  unopn  22845  incld  22985  indiscld  23033  leordtval2  23154  ovolioo  25523  i1f1  25645  aannenlem2  26291  upgrbi  29115  umgrbi  29123  frgr3vlem2  30298  4cycl2v2nb  30313  sshjval3  31378  pr01ssre  32854  psgnid  33128  pmtrto1cl  33130  cnmsgn0g  33177  altgnsg  33180  constrsscn  33846  constrextdg2  33855  mdetpmtr1  33929  mdetpmtr12  33931  esumsnf  34170  prsiga  34237  difelsiga  34239  measssd  34321  carsgsigalem  34421  carsgclctun  34427  pmeasmono  34430  eulerpartlemgs2  34486  eulerpartlemn  34487  probun  34525  signswch  34667  signsvfn  34688  signlem0  34693  breprexpnat  34740  kur14lem1  35349  ssoninhaus  36591  poimirlem15  37775  inidl  38170  pmapmeet  39972  diameetN  41255  dihmeetcN  41501  dihmeet  41542  dvh4dimlem  41642  dvhdimlem  41643  dvh4dimN  41646  dvh3dim3N  41648  lcfrlem23  41764  lcfrlem25  41766  lcfrlem35  41776  mapdindp2  41920  lspindp5  41969  brfvrcld  43874  corclrcl  43890  corcltrcl  43922  ibliooicc  46157  fourierdlem51  46343  fourierdlem64  46356  fourierdlem102  46394  fourierdlem114  46406  sge0sn  46565  ovnsubadd2lem  46831  sprvalpw  47668  prprvalpw  47703  perfectALTVlem2  47910  nnsum3primesgbe  47980  clnbgredg  48028  uhgrimprop  48080  isuspgrimlem  48083  isubgr3stgrlem7  48160  usgrexmpl1lem  48209  usgrexmpl2lem  48214  usgrexmpl2nb1  48220  usgrexmpl2nb2  48221  usgrexmpl2nb4  48223  usgrexmpl2nb5  48224  pgnbgreunbgr  48313  fprmappr  48533  zlmodzxzel  48543  zlmodzxzldeplem1  48688  2arymaptfo  48842  prelrrx2  48901  line2x  48942  line2y  48943  onsetreclem2  49893