Theorem prssi 4788

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3917  {cpr 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-sn 4593  df-pr 4595

This theorem is referenced by:  prssd  4789  tpssi  4805  fr2nr  5618  fprb  7171  f1ofvswap  7284  ordunel  7805  rex2dom  9200  1sdomOLD  9203  dfac2b  10091  tskpr  10730  m1expcl2  14057  m1expcl  14058  wrdlen2i  14915  gcdcllem3  16478  lcmfpr  16604  mreincl  17567  acsfn2  17631  ipole  18500  pmtr3ncom  19412  subrngin  20477  subrgin  20512  lssincl  20878  lspvadd  21010  cnmsgnbas  21494  cnmsgngrp  21495  psgninv  21498  zrhpsgnmhm  21500  mdetunilem7  22512  unopn  22797  incld  22937  indiscld  22985  leordtval2  23106  ovolioo  25476  i1f1  25598  aannenlem2  26244  upgrbi  29027  umgrbi  29035  frgr3vlem2  30210  4cycl2v2nb  30225  sshjval3  31290  pr01ssre  32756  psgnid  33061  pmtrto1cl  33063  cnmsgn0g  33110  altgnsg  33113  constrsscn  33737  constrextdg2  33746  mdetpmtr1  33820  mdetpmtr12  33822  esumsnf  34061  prsiga  34128  difelsiga  34130  measssd  34212  carsgsigalem  34313  carsgclctun  34319  pmeasmono  34322  eulerpartlemgs2  34378  eulerpartlemn  34379  probun  34417  signswch  34559  signsvfn  34580  signlem0  34585  breprexpnat  34632  kur14lem1  35200  ssoninhaus  36443  poimirlem15  37636  inidl  38031  pmapmeet  39774  diameetN  41057  dihmeetcN  41303  dihmeet  41344  dvh4dimlem  41444  dvhdimlem  41445  dvh4dimN  41448  dvh3dim3N  41450  lcfrlem23  41566  lcfrlem25  41568  lcfrlem35  41578  mapdindp2  41722  lspindp5  41771  brfvrcld  43687  corclrcl  43703  corcltrcl  43735  ibliooicc  45976  fourierdlem51  46162  fourierdlem64  46175  fourierdlem102  46213  fourierdlem114  46225  sge0sn  46384  ovnsubadd2lem  46650  sprvalpw  47485  prprvalpw  47520  perfectALTVlem2  47727  nnsum3primesgbe  47797  clnbgredg  47844  uhgrimprop  47896  isuspgrimlem  47899  isubgr3stgrlem7  47975  usgrexmpl1lem  48016  usgrexmpl2lem  48021  usgrexmpl2nb1  48027  usgrexmpl2nb2  48028  usgrexmpl2nb4  48030  usgrexmpl2nb5  48031  pgnbgreunbgr  48119  fprmappr  48337  zlmodzxzel  48347  zlmodzxzldeplem1  48493  2arymaptfo  48647  prelrrx2  48706  line2x  48747  line2y  48748  onsetreclem2  49699