Theorem prssi 4825

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105   ⊆ wss 3962  {cpr 4632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-ss 3979  df-sn 4631  df-pr 4633

This theorem is referenced by:  prssd  4826  tpssi  4842  fr2nr  5665  fprb  7213  f1ofvswap  7325  ordunel  7846  rex2dom  9279  1sdomOLD  9282  dfac2b  10168  tskpr  10807  m1expcl2  14122  m1expcl  14123  wrdlen2i  14977  gcdcllem3  16534  lcmfpr  16660  mreincl  17643  acsfn2  17707  ipole  18591  pmtr3ncom  19507  subrngin  20577  subrgin  20612  lssincl  20980  lspvadd  21112  cnmsgnbas  21613  cnmsgngrp  21614  psgninv  21617  zrhpsgnmhm  21619  mdetunilem7  22639  unopn  22924  incld  23066  indiscld  23114  leordtval2  23235  ovolioo  25616  i1f1  25738  aannenlem2  26385  upgrbi  29124  umgrbi  29132  frgr3vlem2  30302  4cycl2v2nb  30317  sshjval3  31382  pr01ssre  32830  psgnid  33099  pmtrto1cl  33101  cnmsgn0g  33148  altgnsg  33151  constrsscn  33744  mdetpmtr1  33783  mdetpmtr12  33785  esumsnf  34044  prsiga  34111  difelsiga  34113  measssd  34195  carsgsigalem  34296  carsgclctun  34302  pmeasmono  34305  eulerpartlemgs2  34361  eulerpartlemn  34362  probun  34400  signswch  34554  signsvfn  34575  signlem0  34580  breprexpnat  34627  kur14lem1  35190  ssoninhaus  36430  poimirlem15  37621  inidl  38016  pmapmeet  39755  diameetN  41038  dihmeetcN  41284  dihmeet  41325  dvh4dimlem  41425  dvhdimlem  41426  dvh4dimN  41429  dvh3dim3N  41431  lcfrlem23  41547  lcfrlem25  41549  lcfrlem35  41559  mapdindp2  41703  lspindp5  41752  brfvrcld  43680  corclrcl  43696  corcltrcl  43728  ibliooicc  45926  fourierdlem51  46112  fourierdlem64  46125  fourierdlem102  46163  fourierdlem114  46175  sge0sn  46334  ovnsubadd2lem  46600  sprvalpw  47404  prprvalpw  47439  perfectALTVlem2  47646  nnsum3primesgbe  47716  clnbgredg  47763  uspgrimprop  47810  isuspgrimlem  47811  isubgr3stgrlem7  47874  usgrexmpl1lem  47915  usgrexmpl2lem  47920  usgrexmpl2nb1  47926  usgrexmpl2nb2  47927  usgrexmpl2nb4  47929  usgrexmpl2nb5  47930  fprmappr  48189  zlmodzxzel  48199  zlmodzxzldeplem1  48345  2arymaptfo  48503  prelrrx2  48562  line2x  48603  line2y  48604  onsetreclem2  48936