Theorem prssi 4781

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

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

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 3446  df-un 3916  df-ss 3928  df-sn 4586  df-pr 4588

This theorem is referenced by:  prssd  4782  tpssi  4798  fr2nr  5608  fprb  7150  f1ofvswap  7263  ordunel  7782  rex2dom  9169  1sdomOLD  9172  dfac2b  10060  tskpr  10699  m1expcl2  14026  m1expcl  14027  wrdlen2i  14884  gcdcllem3  16447  lcmfpr  16573  mreincl  17536  acsfn2  17604  ipole  18475  pmtr3ncom  19389  subrngin  20481  subrgin  20516  lssincl  20903  lspvadd  21035  cnmsgnbas  21520  cnmsgngrp  21521  psgninv  21524  zrhpsgnmhm  21526  mdetunilem7  22538  unopn  22823  incld  22963  indiscld  23011  leordtval2  23132  ovolioo  25502  i1f1  25624  aannenlem2  26270  upgrbi  29073  umgrbi  29081  frgr3vlem2  30253  4cycl2v2nb  30268  sshjval3  31333  pr01ssre  32799  psgnid  33069  pmtrto1cl  33071  cnmsgn0g  33118  altgnsg  33121  constrsscn  33723  constrextdg2  33732  mdetpmtr1  33806  mdetpmtr12  33808  esumsnf  34047  prsiga  34114  difelsiga  34116  measssd  34198  carsgsigalem  34299  carsgclctun  34305  pmeasmono  34308  eulerpartlemgs2  34364  eulerpartlemn  34365  probun  34403  signswch  34545  signsvfn  34566  signlem0  34571  breprexpnat  34618  kur14lem1  35186  ssoninhaus  36429  poimirlem15  37622  inidl  38017  pmapmeet  39760  diameetN  41043  dihmeetcN  41289  dihmeet  41330  dvh4dimlem  41430  dvhdimlem  41431  dvh4dimN  41434  dvh3dim3N  41436  lcfrlem23  41552  lcfrlem25  41554  lcfrlem35  41564  mapdindp2  41708  lspindp5  41757  brfvrcld  43673  corclrcl  43689  corcltrcl  43721  ibliooicc  45962  fourierdlem51  46148  fourierdlem64  46161  fourierdlem102  46199  fourierdlem114  46211  sge0sn  46370  ovnsubadd2lem  46636  sprvalpw  47474  prprvalpw  47509  perfectALTVlem2  47716  nnsum3primesgbe  47786  clnbgredg  47833  uhgrimprop  47885  isuspgrimlem  47888  isubgr3stgrlem7  47964  usgrexmpl1lem  48005  usgrexmpl2lem  48010  usgrexmpl2nb1  48016  usgrexmpl2nb2  48017  usgrexmpl2nb4  48019  usgrexmpl2nb5  48020  pgnbgreunbgr  48108  fprmappr  48326  zlmodzxzel  48336  zlmodzxzldeplem1  48482  2arymaptfo  48636  prelrrx2  48695  line2x  48736  line2y  48737  onsetreclem2  49688