Theorem prssi 4772

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3903  {cpr 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908  df-ss 3920  df-sn 4578  df-pr 4580

This theorem is referenced by:  prssd  4773  tpssi  4789  fr2nr  5596  fprb  7130  f1ofvswap  7243  ordunel  7760  rex2dom  9142  dfac2b  10025  tskpr  10664  m1expcl2  13992  m1expcl  13993  wrdlen2i  14849  gcdcllem3  16412  lcmfpr  16538  mreincl  17501  acsfn2  17569  ipole  18440  pmtr3ncom  19354  subrngin  20446  subrgin  20481  lssincl  20868  lspvadd  21000  cnmsgnbas  21485  cnmsgngrp  21486  psgninv  21489  zrhpsgnmhm  21491  mdetunilem7  22503  unopn  22788  incld  22928  indiscld  22976  leordtval2  23097  ovolioo  25467  i1f1  25589  aannenlem2  26235  upgrbi  29038  umgrbi  29046  frgr3vlem2  30218  4cycl2v2nb  30233  sshjval3  31298  pr01ssre  32770  psgnid  33040  pmtrto1cl  33042  cnmsgn0g  33089  altgnsg  33092  constrsscn  33713  constrextdg2  33722  mdetpmtr1  33796  mdetpmtr12  33798  esumsnf  34037  prsiga  34104  difelsiga  34106  measssd  34188  carsgsigalem  34289  carsgclctun  34295  pmeasmono  34298  eulerpartlemgs2  34354  eulerpartlemn  34355  probun  34393  signswch  34535  signsvfn  34556  signlem0  34561  breprexpnat  34608  kur14lem1  35189  ssoninhaus  36432  poimirlem15  37625  inidl  38020  pmapmeet  39762  diameetN  41045  dihmeetcN  41291  dihmeet  41332  dvh4dimlem  41432  dvhdimlem  41433  dvh4dimN  41436  dvh3dim3N  41438  lcfrlem23  41554  lcfrlem25  41556  lcfrlem35  41566  mapdindp2  41710  lspindp5  41759  brfvrcld  43674  corclrcl  43690  corcltrcl  43722  ibliooicc  45962  fourierdlem51  46148  fourierdlem64  46161  fourierdlem102  46199  fourierdlem114  46211  sge0sn  46370  ovnsubadd2lem  46636  sprvalpw  47474  prprvalpw  47509  perfectALTVlem2  47716  nnsum3primesgbe  47786  clnbgredg  47834  uhgrimprop  47886  isuspgrimlem  47889  isubgr3stgrlem7  47966  usgrexmpl1lem  48015  usgrexmpl2lem  48020  usgrexmpl2nb1  48026  usgrexmpl2nb2  48027  usgrexmpl2nb4  48029  usgrexmpl2nb5  48030  pgnbgreunbgr  48119  fprmappr  48339  zlmodzxzel  48349  zlmodzxzldeplem1  48495  2arymaptfo  48649  prelrrx2  48708  line2x  48749  line2y  48750  onsetreclem2  49701