Theorem prssi 4789

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146   ⊆ wss 3906  {cpr 4593

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923  df-sn 4592  df-pr 4594

This theorem is used by:  prssd  4790  tpssi  4805  fr2nr  5640  fprb  7198  f1ofvswap  7313  ordunel  7829  rex2dom  9220  dfac2b  10130  tskpr  10772  pr01ssre  11229  m1expcl2  14141  m1expcl  14142  wrdlen2i  15005  gcdcllem3  16583  lcmfpr  16709  mreincl  17675  acsfn2  17743  ipole  18614  pmtr3ncom  19591  subrngin  20712  subrgin  20747  lssincl  21138  lspvadd  21269  cnmsgnbas  21780  cnmsgngrp  21781  psgninv  21784  zrhpsgnmhm  21786  mdetunilem7  22827  unopn  23112  incld  23252  indiscld  23300  leordtval2  23421  ovolioo  25780  i1f1  25902  aannenlem2  26545  upgrbi  29500  umgrbi  29508  frgr3vlem2  30698  4cycl2v2nb  30713  sshjval3  31779  psgnid  33483  pmtrto1cl  33485  cnmsgn0g  33532  altgnsg  33535  inlidl  33795  constrsscn  34196  constrextdg2  34205  mdetpmtr1  34279  mdetpmtr12  34281  esumsnf  34520  prsiga  34587  measssd  34672  carsgsigalem  34772  carsgclctun  34778  pmeasmono  34781  eulerpartlemgs2  34837  eulerpartlemn  34838  probun  34876  signswch  35015  signsvfn  35036  signlem0  35041  breprexpnat  35088  kur14lem1  35737  ssoninhaus  37018  poimirlem15  38345  inidl  38741  pmapmeet  40607  diameetN  41890  dihmeetcN  42136  dihmeet  42177  dvh4dimlem  42277  dvhdimlem  42278  dvh4dimN  42281  dvh3dim3N  42283  lcfrlem23  42399  lcfrlem25  42401  lcfrlem35  42411  mapdindp2  42555  lspindp5  42604  brfvrcld  44477  corclrcl  44493  corcltrcl  44525  ibliooicc  46745  fourierdlem51  46931  fourierdlem64  46944  fourierdlem102  46982  fourierdlem114  46994  sge0sn  47153  ovnsubadd2lem  47419  sprvalpw  48289  prprvalpw  48324  perfectALTVlem2  48547  nnsum3primesgbe  48617  clnbgredg  48665  uhgrimprop  48717  isuspgrimlem  48720  isubgr3stgrlem7  48797  usgrexmpl1lem  48846  usgrexmpl2lem  48851  usgrexmpl2nb1  48857  usgrexmpl2nb2  48858  usgrexmpl2nb4  48860  usgrexmpl2nb5  48861  pgnbgreunbgr  48950  fprmappr  49184  zlmodzxzel  49194  zlmodzxzldeplem1  49339  2arymaptfo  49493  prelrrx2  49552  line2x  49593  line2y  49594  onsetreclem2  50543