Theorem prssi 4714

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111   ⊆ wss 3881  {cpr 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528

This theorem is referenced by:  prssd  4715  tpssi  4729  fr2nr  5497  fprb  6933  ordunel  7522  1sdom  8705  dfac2b  9541  tskpr  10181  m1expcl2  13447  m1expcl  13448  wrdlen2i  14295  gcdcllem3  15840  lcmfpr  15961  mreincl  16862  acsfn2  16926  ipole  17760  pmtr3ncom  18595  subrgin  19551  lssincl  19730  lspvadd  19861  cnmsgnbas  20267  cnmsgngrp  20268  psgninv  20271  zrhpsgnmhm  20273  mdetunilem7  21223  unopn  21508  incld  21648  indiscld  21696  leordtval2  21817  ovolioo  24172  i1f1  24294  aannenlem2  24925  upgrbi  26886  umgrbi  26894  frgr3vlem2  28059  4cycl2v2nb  28074  sshjval3  29137  pr01ssre  30566  psgnid  30789  pmtrto1cl  30791  cnmsgn0g  30838  altgnsg  30841  mdetpmtr1  31176  mdetpmtr12  31178  esumsnf  31433  prsiga  31500  difelsiga  31502  measssd  31584  carsgsigalem  31683  carsgclctun  31689  pmeasmono  31692  eulerpartlemgs2  31748  eulerpartlemn  31749  probun  31787  signswch  31941  signsvfn  31962  signlem0  31967  breprexpnat  32015  kur14lem1  32566  ssoninhaus  33909  poimirlem15  35072  inidl  35468  pmapmeet  37069  diameetN  38352  dihmeetcN  38598  dihmeet  38639  dvh4dimlem  38739  dvhdimlem  38740  dvh4dimN  38743  dvh3dim3N  38745  lcfrlem23  38861  lcfrlem25  38863  lcfrlem35  38873  mapdindp2  39017  lspindp5  39066  brfvrcld  40392  corclrcl  40408  corcltrcl  40440  ibliooicc  42613  fourierdlem51  42799  fourierdlem64  42812  fourierdlem102  42850  fourierdlem114  42862  sge0sn  43018  ovnsubadd2lem  43284  sprvalpw  43997  prprvalpw  44032  perfectALTVlem2  44240  nnsum3primesgbe  44310  fprmappr  44747  zlmodzxzel  44757  zlmodzxzldeplem1  44909  2arymaptfo  45068  prelrrx2  45127  line2x  45168  line2y  45169  onsetreclem2  45235