Theorem prssi 4846

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ⊆ wss 3976  {cpr 4650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-sn 4649  df-pr 4651

This theorem is referenced by:  prssd  4847  tpssi  4863  fr2nr  5677  fprb  7231  f1ofvswap  7342  ordunel  7863  rex2dom  9309  1sdomOLD  9312  dfac2b  10200  tskpr  10839  m1expcl2  14136  m1expcl  14137  wrdlen2i  14991  gcdcllem3  16547  lcmfpr  16674  mreincl  17657  acsfn2  17721  ipole  18604  pmtr3ncom  19517  subrngin  20587  subrgin  20624  lssincl  20986  lspvadd  21118  cnmsgnbas  21619  cnmsgngrp  21620  psgninv  21623  zrhpsgnmhm  21625  mdetunilem7  22645  unopn  22930  incld  23072  indiscld  23120  leordtval2  23241  ovolioo  25622  i1f1  25744  aannenlem2  26389  upgrbi  29128  umgrbi  29136  frgr3vlem2  30306  4cycl2v2nb  30321  sshjval3  31386  pr01ssre  32828  psgnid  33090  pmtrto1cl  33092  cnmsgn0g  33139  altgnsg  33142  constrsscn  33730  mdetpmtr1  33769  mdetpmtr12  33771  esumsnf  34028  prsiga  34095  difelsiga  34097  measssd  34179  carsgsigalem  34280  carsgclctun  34286  pmeasmono  34289  eulerpartlemgs2  34345  eulerpartlemn  34346  probun  34384  signswch  34538  signsvfn  34559  signlem0  34564  breprexpnat  34611  kur14lem1  35174  ssoninhaus  36414  poimirlem15  37595  inidl  37990  pmapmeet  39730  diameetN  41013  dihmeetcN  41259  dihmeet  41300  dvh4dimlem  41400  dvhdimlem  41401  dvh4dimN  41404  dvh3dim3N  41406  lcfrlem23  41522  lcfrlem25  41524  lcfrlem35  41534  mapdindp2  41678  lspindp5  41727  brfvrcld  43653  corclrcl  43669  corcltrcl  43701  ibliooicc  45892  fourierdlem51  46078  fourierdlem64  46091  fourierdlem102  46129  fourierdlem114  46141  sge0sn  46300  ovnsubadd2lem  46566  sprvalpw  47354  prprvalpw  47389  perfectALTVlem2  47596  nnsum3primesgbe  47666  clnbgredg  47712  uspgrimprop  47757  isuspgrimlem  47758  usgrexmpl1lem  47836  usgrexmpl2lem  47841  usgrexmpl2nb1  47847  usgrexmpl2nb2  47848  usgrexmpl2nb4  47850  usgrexmpl2nb5  47851  fprmappr  48070  zlmodzxzel  48080  zlmodzxzldeplem1  48229  2arymaptfo  48388  prelrrx2  48447  line2x  48488  line2y  48489  onsetreclem2  48798