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  7822  rex2dom  9212  dfac2b  10113  tskpr  10754  pr01ssre  11211  m1expcl2  14120  m1expcl  14121  wrdlen2i  14978  gcdcllem3  16558  lcmfpr  16684  mreincl  17650  acsfn2  17718  ipole  18589  pmtr3ncom  19544  subrngin  20645  subrgin  20680  lssincl  21063  lspvadd  21194  cnmsgnbas  21696  cnmsgngrp  21697  psgninv  21700  zrhpsgnmhm  21702  mdetunilem7  22743  unopn  23028  incld  23168  indiscld  23216  leordtval2  23337  ovolioo  25695  i1f1  25817  aannenlem2  26458  upgrbi  29383  umgrbi  29391  frgr3vlem2  30565  4cycl2v2nb  30580  sshjval3  31646  psgnid  33357  pmtrto1cl  33359  cnmsgn0g  33406  altgnsg  33409  inlidl  33672  constrsscn  34074  constrextdg2  34083  mdetpmtr1  34157  mdetpmtr12  34159  esumsnf  34398  prsiga  34465  difelsiga  34467  measssd  34549  carsgsigalem  34649  carsgclctun  34655  pmeasmono  34658  eulerpartlemgs2  34714  eulerpartlemn  34715  probun  34753  signswch  34892  signsvfn  34913  signlem0  34918  breprexpnat  34965  kur14lem1  35596  ssoninhaus  36847  poimirlem15  38173  inidl  38568  pmapmeet  40436  diameetN  41719  dihmeetcN  41965  dihmeet  42006  dvh4dimlem  42106  dvhdimlem  42107  dvh4dimN  42110  dvh3dim3N  42112  lcfrlem23  42228  lcfrlem25  42230  lcfrlem35  42240  mapdindp2  42384  lspindp5  42433  brfvrcld  44308  corclrcl  44324  corcltrcl  44356  ibliooicc  46576  fourierdlem51  46762  fourierdlem64  46775  fourierdlem102  46813  fourierdlem114  46825  sge0sn  46984  ovnsubadd2lem  47250  sprvalpw  48117  prprvalpw  48152  perfectALTVlem2  48375  nnsum3primesgbe  48445  clnbgredg  48493  uhgrimprop  48545  isuspgrimlem  48548  isubgr3stgrlem7  48625  usgrexmpl1lem  48674  usgrexmpl2lem  48679  usgrexmpl2nb1  48685  usgrexmpl2nb2  48686  usgrexmpl2nb4  48688  usgrexmpl2nb5  48689  pgnbgreunbgr  48778  fprmappr  49009  zlmodzxzel  49019  zlmodzxzldeplem1  49164  2arymaptfo  49318  prelrrx2  49377  line2x  49418  line2y  49419  onsetreclem2  50368