Theorem prssi 4821

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968  df-sn 4627  df-pr 4629

This theorem is referenced by:  prssd  4822  tpssi  4838  fr2nr  5662  fprb  7214  f1ofvswap  7326  ordunel  7847  rex2dom  9282  1sdomOLD  9285  dfac2b  10171  tskpr  10810  m1expcl2  14126  m1expcl  14127  wrdlen2i  14981  gcdcllem3  16538  lcmfpr  16664  mreincl  17642  acsfn2  17706  ipole  18579  pmtr3ncom  19493  subrngin  20561  subrgin  20596  lssincl  20963  lspvadd  21095  cnmsgnbas  21596  cnmsgngrp  21597  psgninv  21600  zrhpsgnmhm  21602  mdetunilem7  22624  unopn  22909  incld  23051  indiscld  23099  leordtval2  23220  ovolioo  25603  i1f1  25725  aannenlem2  26371  upgrbi  29110  umgrbi  29118  frgr3vlem2  30293  4cycl2v2nb  30308  sshjval3  31373  pr01ssre  32826  psgnid  33117  pmtrto1cl  33119  cnmsgn0g  33166  altgnsg  33169  constrsscn  33781  constrextdg2  33790  mdetpmtr1  33822  mdetpmtr12  33824  esumsnf  34065  prsiga  34132  difelsiga  34134  measssd  34216  carsgsigalem  34317  carsgclctun  34323  pmeasmono  34326  eulerpartlemgs2  34382  eulerpartlemn  34383  probun  34421  signswch  34576  signsvfn  34597  signlem0  34602  breprexpnat  34649  kur14lem1  35211  ssoninhaus  36449  poimirlem15  37642  inidl  38037  pmapmeet  39775  diameetN  41058  dihmeetcN  41304  dihmeet  41345  dvh4dimlem  41445  dvhdimlem  41446  dvh4dimN  41449  dvh3dim3N  41451  lcfrlem23  41567  lcfrlem25  41569  lcfrlem35  41579  mapdindp2  41723  lspindp5  41772  brfvrcld  43704  corclrcl  43720  corcltrcl  43752  ibliooicc  45986  fourierdlem51  46172  fourierdlem64  46185  fourierdlem102  46223  fourierdlem114  46235  sge0sn  46394  ovnsubadd2lem  46660  sprvalpw  47467  prprvalpw  47502  perfectALTVlem2  47709  nnsum3primesgbe  47779  clnbgredg  47826  uspgrimprop  47873  isuspgrimlem  47874  isubgr3stgrlem7  47939  usgrexmpl1lem  47980  usgrexmpl2lem  47985  usgrexmpl2nb1  47991  usgrexmpl2nb2  47992  usgrexmpl2nb4  47994  usgrexmpl2nb5  47995  fprmappr  48261  zlmodzxzel  48271  zlmodzxzldeplem1  48417  2arymaptfo  48575  prelrrx2  48634  line2x  48675  line2y  48676  onsetreclem2  49225