Theorem prssi 4772

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

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

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-ss 3915  df-sn 4576  df-pr 4578

This theorem is referenced by:  prssd  4773  tpssi  4789  fr2nr  5596  fprb  7134  f1ofvswap  7246  ordunel  7763  rex2dom  9144  dfac2b  10029  tskpr  10668  m1expcl2  13994  m1expcl  13995  wrdlen2i  14851  gcdcllem3  16414  lcmfpr  16540  mreincl  17503  acsfn2  17571  ipole  18442  pmtr3ncom  19389  subrngin  20478  subrgin  20513  lssincl  20900  lspvadd  21032  cnmsgnbas  21517  cnmsgngrp  21518  psgninv  21521  zrhpsgnmhm  21523  mdetunilem7  22534  unopn  22819  incld  22959  indiscld  23007  leordtval2  23128  ovolioo  25497  i1f1  25619  aannenlem2  26265  upgrbi  29073  umgrbi  29081  frgr3vlem2  30256  4cycl2v2nb  30271  sshjval3  31336  pr01ssre  32812  psgnid  33073  pmtrto1cl  33075  cnmsgn0g  33122  altgnsg  33125  constrsscn  33774  constrextdg2  33783  mdetpmtr1  33857  mdetpmtr12  33859  esumsnf  34098  prsiga  34165  difelsiga  34167  measssd  34249  carsgsigalem  34349  carsgclctun  34355  pmeasmono  34358  eulerpartlemgs2  34414  eulerpartlemn  34415  probun  34453  signswch  34595  signsvfn  34616  signlem0  34621  breprexpnat  34668  kur14lem1  35271  ssoninhaus  36513  poimirlem15  37695  inidl  38090  pmapmeet  39892  diameetN  41175  dihmeetcN  41421  dihmeet  41462  dvh4dimlem  41562  dvhdimlem  41563  dvh4dimN  41566  dvh3dim3N  41568  lcfrlem23  41684  lcfrlem25  41686  lcfrlem35  41696  mapdindp2  41840  lspindp5  41889  brfvrcld  43808  corclrcl  43824  corcltrcl  43856  ibliooicc  46093  fourierdlem51  46279  fourierdlem64  46292  fourierdlem102  46330  fourierdlem114  46342  sge0sn  46501  ovnsubadd2lem  46767  sprvalpw  47604  prprvalpw  47639  perfectALTVlem2  47846  nnsum3primesgbe  47916  clnbgredg  47964  uhgrimprop  48016  isuspgrimlem  48019  isubgr3stgrlem7  48096  usgrexmpl1lem  48145  usgrexmpl2lem  48150  usgrexmpl2nb1  48156  usgrexmpl2nb2  48157  usgrexmpl2nb4  48159  usgrexmpl2nb5  48160  pgnbgreunbgr  48249  fprmappr  48469  zlmodzxzel  48479  zlmodzxzldeplem1  48625  2arymaptfo  48779  prelrrx2  48838  line2x  48879  line2y  48880  onsetreclem2  49831