Theorem prssi 4756

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114   ⊆ wss 3938  {cpr 4571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943  df-in 3945  df-ss 3954  df-sn 4570  df-pr 4572

This theorem is referenced by:  prssd  4757  tpssi  4771  fr2nr  5535  fprb  6958  ordunel  7544  1sdom  8723  dfac2b  9558  tskpr  10194  m1expcl2  13454  m1expcl  13455  wrdlen2i  14306  gcdcllem3  15852  lcmfpr  15973  mreincl  16872  acsfn2  16936  ipole  17770  pmtr3ncom  18605  subrgin  19560  lssincl  19739  lspvadd  19870  cnmsgnbas  20724  cnmsgngrp  20725  psgninv  20728  zrhpsgnmhm  20730  mdetunilem7  21229  unopn  21513  incld  21653  indiscld  21701  leordtval2  21822  ovolioo  24171  i1f1  24293  aannenlem2  24920  upgrbi  26880  umgrbi  26888  frgr3vlem2  28055  4cycl2v2nb  28070  sshjval3  29133  pr01ssre  30542  psgnid  30741  pmtrto1cl  30743  cnmsgn0g  30790  altgnsg  30793  mdetpmtr1  31090  mdetpmtr12  31092  esumsnf  31325  prsiga  31392  difelsiga  31394  inelpisys  31415  measssd  31476  carsgsigalem  31575  carsgclctun  31581  pmeasmono  31584  eulerpartlemgs2  31640  eulerpartlemn  31641  probun  31679  signswch  31833  signsvfn  31854  signlem0  31859  breprexpnat  31907  kur14lem1  32455  ssoninhaus  33798  poimirlem15  34909  inidl  35310  pmapmeet  36911  diameetN  38194  dihmeetcN  38440  dihmeet  38481  dvh4dimlem  38581  dvhdimlem  38582  dvh4dimN  38585  dvh3dim3N  38587  lcfrlem23  38703  lcfrlem25  38705  lcfrlem35  38715  mapdindp2  38859  lspindp5  38908  brfvrcld  40043  corclrcl  40059  corcltrcl  40091  ibliooicc  42263  fourierdlem51  42449  fourierdlem64  42462  fourierdlem102  42500  fourierdlem114  42512  sge0sn  42668  ovnsubadd2lem  42934  sprvalpw  43649  prprvalpw  43684  perfectALTVlem2  43894  nnsum3primesgbe  43964  mapprop  44401  zlmodzxzel  44410  zlmodzxzldeplem1  44562  prelrrx2  44707  line2x  44748  line2y  44749  onsetreclem2  44815