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 269	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2142   ⊆ wss 3904  {cpr 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-ss 3921  df-sn 4583  df-pr 4585

This theorem is referenced by:  prssd  4780  tpssi  4796  fr2nr  5624  fprb  7178  f1ofvswap  7290  ordunel  7807  rex2dom  9197  dfac2b  10087  tskpr  10728  pr01ssre  11185  m1expcl2  14098  m1expcl  14099  wrdlen2i  14955  gcdcllem3  16535  lcmfpr  16661  mreincl  17627  acsfn2  17695  ipole  18566  pmtr3ncom  19515  subrngin  20611  subrgin  20646  lssincl  21032  lspvadd  21163  cnmsgnbas  21630  cnmsgngrp  21631  psgninv  21634  zrhpsgnmhm  21636  mdetunilem7  22678  unopn  22963  incld  23103  indiscld  23151  leordtval2  23272  ovolioo  25630  i1f1  25752  aannenlem2  26393  upgrbi  29294  umgrbi  29302  frgr3vlem2  30476  4cycl2v2nb  30491  sshjval3  31557  psgnid  33277  pmtrto1cl  33279  cnmsgn0g  33326  altgnsg  33329  constrsscn  34037  constrextdg2  34046  mdetpmtr1  34120  mdetpmtr12  34122  esumsnf  34361  prsiga  34428  difelsiga  34430  measssd  34512  carsgsigalem  34612  carsgclctun  34618  pmeasmono  34621  eulerpartlemgs2  34677  eulerpartlemn  34678  probun  34716  signswch  34855  signsvfn  34876  signlem0  34881  breprexpnat  34928  kur14lem1  35556  ssoninhaus  36808  poimirlem15  38134  inidl  38529  pmapmeet  40397  diameetN  41680  dihmeetcN  41926  dihmeet  41967  dvh4dimlem  42067  dvhdimlem  42068  dvh4dimN  42071  dvh3dim3N  42073  lcfrlem23  42189  lcfrlem25  42191  lcfrlem35  42201  mapdindp2  42345  lspindp5  42394  brfvrcld  44267  corclrcl  44283  corcltrcl  44315  ibliooicc  46545  fourierdlem51  46731  fourierdlem64  46744  fourierdlem102  46782  fourierdlem114  46794  sge0sn  46953  ovnsubadd2lem  47219  sprvalpw  48086  prprvalpw  48121  perfectALTVlem2  48344  nnsum3primesgbe  48414  clnbgredg  48462  uhgrimprop  48514  isuspgrimlem  48517  isubgr3stgrlem7  48594  usgrexmpl1lem  48643  usgrexmpl2lem  48648  usgrexmpl2nb1  48654  usgrexmpl2nb2  48655  usgrexmpl2nb4  48657  usgrexmpl2nb5  48658  pgnbgreunbgr  48747  fprmappr  48967  zlmodzxzel  48977  zlmodzxzldeplem1  49122  2arymaptfo  49276  prelrrx2  49335  line2x  49376  line2y  49377  onsetreclem2  50327