Theorem prssi 4818

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106   ⊆ wss 3945  {cpr 4625

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3950  df-in 3952  df-ss 3962  df-sn 4624  df-pr 4626

This theorem is referenced by:  prssd  4819  tpssi  4833  fr2nr  5648  fprb  7180  f1ofvswap  7289  ordunel  7799  rex2dom  9231  1sdomOLD  9234  dfac2b  10109  tskpr  10749  m1expcl2  14035  m1expcl  14036  wrdlen2i  14877  gcdcllem3  16426  lcmfpr  16548  mreincl  17527  acsfn2  17591  ipole  18471  pmtr3ncom  19309  subrgin  20338  lssincl  20527  lspvadd  20658  cnmsgnbas  21066  cnmsgngrp  21067  psgninv  21070  zrhpsgnmhm  21072  mdetunilem7  22051  unopn  22336  incld  22478  indiscld  22526  leordtval2  22647  ovolioo  25016  i1f1  25138  aannenlem2  25773  upgrbi  28282  umgrbi  28290  frgr3vlem2  29456  4cycl2v2nb  29471  sshjval3  30534  pr01ssre  31965  psgnid  32191  pmtrto1cl  32193  cnmsgn0g  32240  altgnsg  32243  mdetpmtr1  32698  mdetpmtr12  32700  esumsnf  32957  prsiga  33024  difelsiga  33026  measssd  33108  carsgsigalem  33209  carsgclctun  33215  pmeasmono  33218  eulerpartlemgs2  33274  eulerpartlemn  33275  probun  33313  signswch  33467  signsvfn  33488  signlem0  33493  breprexpnat  33541  kur14lem1  34092  ssoninhaus  35201  poimirlem15  36371  inidl  36767  pmapmeet  38513  diameetN  39796  dihmeetcN  40042  dihmeet  40083  dvh4dimlem  40183  dvhdimlem  40184  dvh4dimN  40187  dvh3dim3N  40189  lcfrlem23  40305  lcfrlem25  40307  lcfrlem35  40317  mapdindp2  40461  lspindp5  40510  brfvrcld  42277  corclrcl  42293  corcltrcl  42325  ibliooicc  44524  fourierdlem51  44710  fourierdlem64  44723  fourierdlem102  44761  fourierdlem114  44773  sge0sn  44932  ovnsubadd2lem  45198  sprvalpw  45984  prprvalpw  46019  perfectALTVlem2  46226  nnsum3primesgbe  46296  fprmappr  46733  zlmodzxzel  46743  zlmodzxzldeplem1  46893  2arymaptfo  47052  prelrrx2  47111  line2x  47152  line2y  47153  onsetreclem2  47463