Theorem prssi 4293

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977   ⊆ wss 3540  {cpr 4127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-sn 4126  df-pr 4128

This theorem is referenced by:  prssd  4294  tpssi  4309  fr2nr  5016  f1prex  6439  fveqf1o  6457  fr3nr  6871  ordunel  6919  1sdom  8048  en2eqpr  8713  en2eleq  8714  r0weon  8718  dfac2  8836  wuncval2  9448  tskpr  9471  m1expcl2  12744  m1expcl  12745  wrdlen2i  13534  gcdcllem3  15061  lcmfpr  15178  1idssfct  15231  mreincl  16082  mrcun  16105  acsfn2  16147  joinval2  16832  meetval2  16846  ipole  16981  pmtrprfv  17696  pmtrprfv3  17697  symggen  17713  pmtr3ncomlem1  17716  pmtr3ncom  17718  psgnunilem1  17736  subrgin  18626  lssincl  18786  lspprcl  18799  lsptpcl  18800  lspprid1  18818  lspvadd  18917  lsppratlem2  18969  lsppratlem4  18971  cnmsgnbas  19743  cnmsgngrp  19744  psgninv  19747  zrhpsgnmhm  19749  mdetralt  20233  mdetunilem7  20243  unopn  20533  pptbas  20622  incld  20657  indiscld  20705  leordtval2  20826  iscon2  21027  xpsdsval  21996  ovolioo  23143  i1f1  23263  itgioo  23388  aannenlem2  23888  wilthlem2  24595  perfectlem2  24755  upgrbi  25760  umgrbi  25767  umgraex  25852  umgra1  25855  uslgra1  25901  constr1trl  26118  constr3trllem3  26180  nbhashuvtx1  26442  eupath2  26507  umgrabi  26510  konigsberg  26514  frgra3vlem2  26528  4cycl2v2nb  26543  sshjval3  27597  psgnid  29178  pmtrto1cl  29180  mdetpmtr1  29217  mdetpmtr12  29219  pr01ssre  29407  esumsnf  29453  prsiga  29521  difelsiga  29523  inelpisys  29544  measssd  29605  carsgsigalem  29704  carsgclctun  29710  pmeasmono  29713  eulerpartlemgs2  29769  eulerpartlemn  29770  probun  29808  signswch  29964  signsvfn  29985  signlem0  29990  kur14lem1  30442  fprb  30916  ssoninhaus  31617  poimirlem15  32594  inidl  32999  pmapmeet  34077  diameetN  35363  dihmeetcN  35609  dihmeet  35650  dvh4dimlem  35750  dvhdimlem  35751  dvh4dimN  35754  dvh3dim3N  35756  lcfrlem23  35872  lcfrlem25  35874  lcfrlem35  35884  mapdindp2  36028  lspindp5  36077  brfvrcld  37002  corclrcl  37018  corcltrcl  37050  ibliooicc  38863  fourierdlem51  39050  fourierdlem64  39063  fourierdlem102  39101  fourierdlem114  39113  sge0sn  39272  ovnsubadd2lem  39535  perfectALTVlem2  40165  nnsum3primesgbe  40208  frgr3vlem2  41444  4cycl2v2nb-av  41459  mapprop  41917  zlmodzxzel  41926  zlmodzxzldeplem1  42083  onsetreclem2  42248