Theorem prssi 4759

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3891  {cpr 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-un 3896  df-in 3898  df-ss 3908  df-sn 4567  df-pr 4569

This theorem is referenced by:  prssd  4760  tpssi  4774  fr2nr  5566  fprb  7063  f1ofvswap  7171  ordunel  7662  1sdom  8987  dfac2b  9870  tskpr  10510  m1expcl2  13785  m1expcl  13786  wrdlen2i  14636  gcdcllem3  16189  lcmfpr  16313  mreincl  17289  acsfn2  17353  ipole  18233  pmtr3ncom  19064  subrgin  20028  lssincl  20208  lspvadd  20339  cnmsgnbas  20764  cnmsgngrp  20765  psgninv  20768  zrhpsgnmhm  20770  mdetunilem7  21748  unopn  22033  incld  22175  indiscld  22223  leordtval2  22344  ovolioo  24713  i1f1  24835  aannenlem2  25470  upgrbi  27444  umgrbi  27452  frgr3vlem2  28617  4cycl2v2nb  28632  sshjval3  29695  pr01ssre  31117  psgnid  31343  pmtrto1cl  31345  cnmsgn0g  31392  altgnsg  31395  mdetpmtr1  31752  mdetpmtr12  31754  esumsnf  32011  prsiga  32078  difelsiga  32080  measssd  32162  carsgsigalem  32261  carsgclctun  32267  pmeasmono  32270  eulerpartlemgs2  32326  eulerpartlemn  32327  probun  32365  signswch  32519  signsvfn  32540  signlem0  32545  breprexpnat  32593  kur14lem1  33147  ssoninhaus  34616  poimirlem15  35771  inidl  36167  pmapmeet  37766  diameetN  39049  dihmeetcN  39295  dihmeet  39336  dvh4dimlem  39436  dvhdimlem  39437  dvh4dimN  39440  dvh3dim3N  39442  lcfrlem23  39558  lcfrlem25  39560  lcfrlem35  39570  mapdindp2  39714  lspindp5  39763  brfvrcld  41252  corclrcl  41268  corcltrcl  41300  ibliooicc  43466  fourierdlem51  43652  fourierdlem64  43665  fourierdlem102  43703  fourierdlem114  43715  sge0sn  43871  ovnsubadd2lem  44137  sprvalpw  44884  prprvalpw  44919  perfectALTVlem2  45126  nnsum3primesgbe  45196  fprmappr  45633  zlmodzxzel  45643  zlmodzxzldeplem1  45793  2arymaptfo  45952  prelrrx2  46011  line2x  46052  line2y  46053  onsetreclem2  46363