Theorem prssi 4820

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2099   ⊆ wss 3945  {cpr 4626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-un 3950  df-in 3952  df-ss 3962  df-sn 4625  df-pr 4627

This theorem is referenced by:  prssd  4821  tpssi  4835  fr2nr  5650  fprb  7200  f1ofvswap  7309  ordunel  7824  rex2dom  9264  1sdomOLD  9267  dfac2b  10147  tskpr  10787  m1expcl2  14076  m1expcl  14077  wrdlen2i  14919  gcdcllem3  16469  lcmfpr  16591  mreincl  17572  acsfn2  17636  ipole  18519  pmtr3ncom  19423  subrngin  20491  subrgin  20528  lssincl  20842  lspvadd  20974  cnmsgnbas  21503  cnmsgngrp  21504  psgninv  21507  zrhpsgnmhm  21509  mdetunilem7  22513  unopn  22798  incld  22940  indiscld  22988  leordtval2  23109  ovolioo  25490  i1f1  25612  aannenlem2  26257  upgrbi  28899  umgrbi  28907  frgr3vlem2  30077  4cycl2v2nb  30092  sshjval3  31157  pr01ssre  32581  psgnid  32812  pmtrto1cl  32814  cnmsgn0g  32861  altgnsg  32864  mdetpmtr1  33418  mdetpmtr12  33420  esumsnf  33677  prsiga  33744  difelsiga  33746  measssd  33828  carsgsigalem  33929  carsgclctun  33935  pmeasmono  33938  eulerpartlemgs2  33994  eulerpartlemn  33995  probun  34033  signswch  34187  signsvfn  34208  signlem0  34213  breprexpnat  34260  kur14lem1  34810  ssoninhaus  35926  poimirlem15  37102  inidl  37497  pmapmeet  39240  diameetN  40523  dihmeetcN  40769  dihmeet  40810  dvh4dimlem  40910  dvhdimlem  40911  dvh4dimN  40914  dvh3dim3N  40916  lcfrlem23  41032  lcfrlem25  41034  lcfrlem35  41044  mapdindp2  41188  lspindp5  41237  brfvrcld  43115  corclrcl  43131  corcltrcl  43163  ibliooicc  45353  fourierdlem51  45539  fourierdlem64  45552  fourierdlem102  45590  fourierdlem114  45602  sge0sn  45761  ovnsubadd2lem  46027  sprvalpw  46814  prprvalpw  46849  perfectALTVlem2  47056  nnsum3primesgbe  47126  uspgrimprop  47165  isuspgrimlem  47166  fprmappr  47403  zlmodzxzel  47413  zlmodzxzldeplem1  47562  2arymaptfo  47721  prelrrx2  47780  line2x  47821  line2y  47822  onsetreclem2  48131