Theorem prssi 4791

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149   ⊆ wss 3913  {cpr 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930  df-sn 4595  df-pr 4597

This theorem is referenced by:  prssd  4792  tpssi  4807  fr2nr  5639  fprb  7193  f1ofvswap  7305  ordunel  7823  rex2dom  9213  dfac2b  10114  tskpr  10755  pr01ssre  11212  m1expcl2  14121  m1expcl  14122  wrdlen2i  14979  gcdcllem3  16559  lcmfpr  16685  mreincl  17651  acsfn2  17719  ipole  18590  pmtr3ncom  19545  subrngin  20646  subrgin  20681  lssincl  21064  lspvadd  21195  cnmsgnbas  21697  cnmsgngrp  21698  psgninv  21701  zrhpsgnmhm  21703  mdetunilem7  22744  unopn  23029  incld  23169  indiscld  23217  leordtval2  23338  ovolioo  25696  i1f1  25818  aannenlem2  26459  upgrbi  29384  umgrbi  29392  frgr3vlem2  30566  4cycl2v2nb  30581  sshjval3  31647  psgnid  33358  pmtrto1cl  33360  cnmsgn0g  33407  altgnsg  33410  inlidl  33673  constrsscn  34075  constrextdg2  34084  mdetpmtr1  34158  mdetpmtr12  34160  esumsnf  34399  prsiga  34466  difelsiga  34468  measssd  34550  carsgsigalem  34650  carsgclctun  34656  pmeasmono  34659  eulerpartlemgs2  34715  eulerpartlemn  34716  probun  34754  signswch  34893  signsvfn  34914  signlem0  34919  breprexpnat  34966  kur14lem1  35597  ssoninhaus  36848  poimirlem15  38174  inidl  38569  pmapmeet  40437  diameetN  41720  dihmeetcN  41966  dihmeet  42007  dvh4dimlem  42107  dvhdimlem  42108  dvh4dimN  42111  dvh3dim3N  42113  lcfrlem23  42229  lcfrlem25  42231  lcfrlem35  42241  mapdindp2  42385  lspindp5  42434  brfvrcld  44309  corclrcl  44325  corcltrcl  44357  ibliooicc  46577  fourierdlem51  46763  fourierdlem64  46776  fourierdlem102  46814  fourierdlem114  46826  sge0sn  46985  ovnsubadd2lem  47251  sprvalpw  48118  prprvalpw  48153  perfectALTVlem2  48376  nnsum3primesgbe  48446  clnbgredg  48494  uhgrimprop  48546  isuspgrimlem  48549  isubgr3stgrlem7  48626  usgrexmpl1lem  48675  usgrexmpl2lem  48680  usgrexmpl2nb1  48686  usgrexmpl2nb2  48687  usgrexmpl2nb4  48689  usgrexmpl2nb5  48690  pgnbgreunbgr  48779  fprmappr  49010  zlmodzxzel  49020  zlmodzxzldeplem1  49165  2arymaptfo  49319  prelrrx2  49378  line2x  49419  line2y  49420  onsetreclem2  50369