Theorem prssi 4755

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106   ⊆ wss 3887  {cpr 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3432  df-un 3892  df-in 3894  df-ss 3904  df-sn 4563  df-pr 4565

This theorem is referenced by:  prssd  4756  tpssi  4770  fr2nr  5563  fprb  7062  f1ofvswap  7171  ordunel  7665  1sdom  9013  dfac2b  9874  tskpr  10514  m1expcl2  13792  m1expcl  13793  wrdlen2i  14643  gcdcllem3  16196  lcmfpr  16320  mreincl  17296  acsfn2  17360  ipole  18240  pmtr3ncom  19071  subrgin  20035  lssincl  20215  lspvadd  20346  cnmsgnbas  20771  cnmsgngrp  20772  psgninv  20775  zrhpsgnmhm  20777  mdetunilem7  21755  unopn  22040  incld  22182  indiscld  22230  leordtval2  22351  ovolioo  24720  i1f1  24842  aannenlem2  25477  upgrbi  27451  umgrbi  27459  frgr3vlem2  28624  4cycl2v2nb  28639  sshjval3  29702  pr01ssre  31124  psgnid  31350  pmtrto1cl  31352  cnmsgn0g  31399  altgnsg  31402  mdetpmtr1  31759  mdetpmtr12  31761  esumsnf  32018  prsiga  32085  difelsiga  32087  measssd  32169  carsgsigalem  32268  carsgclctun  32274  pmeasmono  32277  eulerpartlemgs2  32333  eulerpartlemn  32334  probun  32372  signswch  32526  signsvfn  32547  signlem0  32552  breprexpnat  32600  kur14lem1  33154  ssoninhaus  34623  poimirlem15  35778  inidl  36174  pmapmeet  37773  diameetN  39056  dihmeetcN  39302  dihmeet  39343  dvh4dimlem  39443  dvhdimlem  39444  dvh4dimN  39447  dvh3dim3N  39449  lcfrlem23  39565  lcfrlem25  39567  lcfrlem35  39577  mapdindp2  39721  lspindp5  39770  brfvrcld  41258  corclrcl  41274  corcltrcl  41306  ibliooicc  43471  fourierdlem51  43657  fourierdlem64  43670  fourierdlem102  43708  fourierdlem114  43720  sge0sn  43876  ovnsubadd2lem  44142  sprvalpw  44888  prprvalpw  44923  perfectALTVlem2  45130  nnsum3primesgbe  45200  fprmappr  45637  zlmodzxzel  45647  zlmodzxzldeplem1  45797  2arymaptfo  45956  prelrrx2  46015  line2x  46056  line2y  46057  onsetreclem2  46367