Theorem prssi 4498

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2139   ⊆ wss 3715  {cpr 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-un 3720  df-in 3722  df-ss 3729  df-sn 4322  df-pr 4324

This theorem is referenced by:  prssd  4499  tpssi  4514  fr2nr  5244  f1prex  6702  fveqf1o  6720  fr3nr  7144  ordunel  7192  1sdom  8328  en2eqpr  9020  en2eleq  9021  r0weon  9025  dfac2b  9143  dfac2OLD  9145  wuncval2  9761  tskpr  9784  m1expcl2  13076  m1expcl  13077  wrdlen2i  13887  gcdcllem3  15425  lcmfpr  15542  1idssfct  15595  mreincl  16461  mrcun  16484  acsfn2  16525  joinval2  17210  meetval2  17224  ipole  17359  pmtrprfv  18073  pmtrprfv3  18074  symggen  18090  pmtr3ncomlem1  18093  pmtr3ncom  18095  psgnunilem1  18113  subrgin  19005  lssincl  19167  lspprcl  19180  lsptpcl  19181  lspprid1  19199  lspvadd  19298  lsppratlem2  19350  lsppratlem4  19352  cnmsgnbas  20126  cnmsgngrp  20127  psgninv  20130  zrhpsgnmhm  20132  mdetralt  20616  mdetunilem7  20626  unopn  20910  pptbas  21014  incld  21049  indiscld  21097  leordtval2  21218  isconn2  21419  xpsdsval  22387  ovolioo  23536  i1f1  23656  itgioo  23781  aannenlem2  24283  wilthlem2  24994  perfectlem2  25154  upgrbi  26187  umgrbi  26195  frgr3vlem2  27428  4cycl2v2nb  27443  sshjval3  28522  pr01ssre  29879  psgnid  30156  pmtrto1cl  30158  mdetpmtr1  30198  mdetpmtr12  30200  esumsnf  30435  prsiga  30503  difelsiga  30505  inelpisys  30526  measssd  30587  carsgsigalem  30686  carsgclctun  30692  pmeasmono  30695  eulerpartlemgs2  30751  eulerpartlemn  30752  probun  30790  signswch  30947  signsvfn  30968  signlem0  30973  breprexpnat  31021  kur14lem1  31495  fprb  31976  ssoninhaus  32753  poimirlem15  33737  inidl  34142  pmapmeet  35562  diameetN  36847  dihmeetcN  37093  dihmeet  37134  dvh4dimlem  37234  dvhdimlem  37235  dvh4dimN  37238  dvh3dim3N  37240  lcfrlem23  37356  lcfrlem25  37358  lcfrlem35  37368  mapdindp2  37512  lspindp5  37561  brfvrcld  38485  corclrcl  38501  corcltrcl  38533  ibliooicc  40690  fourierdlem51  40877  fourierdlem64  40890  fourierdlem102  40928  fourierdlem114  40940  sge0sn  41099  ovnsubadd2lem  41365  perfectALTVlem2  42141  nnsum3primesgbe  42190  sprvalpw  42240  mapprop  42634  zlmodzxzel  42643  zlmodzxzldeplem1  42799  onsetreclem2  42962