Theorem prssi 4779

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146   ⊆ wss 3899  {cpr 4589

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-ss 3900  df-un 4153  df-sn 4588  df-pr 4590

This theorem is used by:  prssd  4780  tpssi  4795  fr2nr  5631  fprb  7206  f1ofvswap  7321  ordunel  7845  rex2dom  9255  dfac2b  10219  tskpr  10865  pr01ssre  11322  m1expcl2  14238  m1expcl  14239  wrdlen2i  15105  gcdcllem3  16683  lcmfpr  16814  mreincl  17781  acsfn2  17849  ipole  18720  pmtr3ncom  19701  subrngin  20825  subrgin  20860  lssincl  21252  lspvadd  21383  cnmsgnbas  21896  cnmsgngrp  21897  psgninv  21900  zrhpsgnmhm  21902  mdetunilem7  22945  unopn  23233  incld  23373  indiscld  23421  leordtval2  23542  ovolioo  25901  i1f1  26023  aannenlem2  26668  upgrbi  29683  umgrbi  29691  frgr3vlem2  30887  4cycl2v2nb  30902  sshjval3  31968  psgnid  33711  pmtrto1cl  33713  cnmsgn0g  33760  altgnsg  33763  inlidl  34024  constrsscn  34425  constrextdg2  34434  mdetpmtr1  34508  mdetpmtr12  34510  esumsnf  34749  prsiga  34816  measssd  34901  carsgsigalem  35000  carsgclctun  35006  pmeasmono  35009  eulerpartlemgs2  35065  eulerpartlemn  35066  probun  35104  signswch  35243  signsvfn  35264  signlem0  35269  breprexpnat  35316  kur14lem1  36092  ssoninhaus  37363  poimirlem15  38693  impprop  38784  inidl  39104  pmapmeet  40970  diameetN  42253  dihmeetcN  42499  dihmeet  42540  dvh4dimlem  42640  dvhdimlem  42641  dvh4dimN  42644  dvh3dim3N  42646  lcfrlem23  42762  lcfrlem25  42764  lcfrlem35  42774  mapdindp2  42918  lspindp5  42967  brfvrcld  44831  corclrcl  44847  corcltrcl  44879  ibliooicc  47120  fourierdlem51  47306  fourierdlem64  47319  fourierdlem102  47357  fourierdlem114  47369  sge0sn  47528  ovnsubadd2lem  47794  sprvalpw  48701  prprvalpw  48736  perfectALTVlem2  48959  nnsum3primesgbe  49029  clnbgredg  49077  uhgrimprop  49129  isuspgrimlem  49132  isubgr3stgrlem7  49209  usgrexmpl1lem  49258  usgrexmpl2lem  49263  usgrexmpl2nb1  49269  usgrexmpl2nb2  49270  usgrexmpl2nb4  49272  usgrexmpl2nb5  49273  pgnbgreunbgr  49362  fprmappr  49596  zlmodzxzel  49606  zlmodzxzldeplem1  49751  2arymaptfo  49905  onsetreclem2  51013