Theorem prssi 4764

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3889  {cpr 4569

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-sn 4568  df-pr 4570

This theorem is referenced by:  prssd  4765  tpssi  4781  fr2nr  5608  fprb  7149  f1ofvswap  7261  ordunel  7778  rex2dom  9163  dfac2b  10053  tskpr  10693  pr01ssre  11148  m1expcl2  14047  m1expcl  14048  wrdlen2i  14904  gcdcllem3  16470  lcmfpr  16596  mreincl  17561  acsfn2  17629  ipole  18500  pmtr3ncom  19450  subrngin  20538  subrgin  20573  lssincl  20960  lspvadd  21091  cnmsgnbas  21558  cnmsgngrp  21559  psgninv  21562  zrhpsgnmhm  21564  mdetunilem7  22583  unopn  22868  incld  23008  indiscld  23056  leordtval2  23177  ovolioo  25535  i1f1  25657  aannenlem2  26295  upgrbi  29162  umgrbi  29170  frgr3vlem2  30344  4cycl2v2nb  30359  sshjval3  31425  psgnid  33158  pmtrto1cl  33160  cnmsgn0g  33207  altgnsg  33210  constrsscn  33884  constrextdg2  33893  mdetpmtr1  33967  mdetpmtr12  33969  esumsnf  34208  prsiga  34275  difelsiga  34277  measssd  34359  carsgsigalem  34459  carsgclctun  34465  pmeasmono  34468  eulerpartlemgs2  34524  eulerpartlemn  34525  probun  34563  signswch  34705  signsvfn  34726  signlem0  34731  breprexpnat  34778  kur14lem1  35388  ssoninhaus  36630  poimirlem15  37956  inidl  38351  pmapmeet  40219  diameetN  41502  dihmeetcN  41748  dihmeet  41789  dvh4dimlem  41889  dvhdimlem  41890  dvh4dimN  41893  dvh3dim3N  41895  lcfrlem23  42011  lcfrlem25  42013  lcfrlem35  42023  mapdindp2  42167  lspindp5  42216  brfvrcld  44118  corclrcl  44134  corcltrcl  44166  ibliooicc  46399  fourierdlem51  46585  fourierdlem64  46598  fourierdlem102  46636  fourierdlem114  46648  sge0sn  46807  ovnsubadd2lem  47073  sprvalpw  47940  prprvalpw  47975  perfectALTVlem2  48198  nnsum3primesgbe  48268  clnbgredg  48316  uhgrimprop  48368  isuspgrimlem  48371  isubgr3stgrlem7  48448  usgrexmpl1lem  48497  usgrexmpl2lem  48502  usgrexmpl2nb1  48508  usgrexmpl2nb2  48509  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  pgnbgreunbgr  48601  fprmappr  48821  zlmodzxzel  48831  zlmodzxzldeplem1  48976  2arymaptfo  49130  prelrrx2  49189  line2x  49230  line2y  49231  onsetreclem2  50181