Theorem prssi 4785

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

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

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 3449  df-un 3919  df-ss 3931  df-sn 4590  df-pr 4592

This theorem is referenced by:  prssd  4786  tpssi  4802  fr2nr  5615  fprb  7168  f1ofvswap  7281  ordunel  7802  rex2dom  9193  1sdomOLD  9196  dfac2b  10084  tskpr  10723  m1expcl2  14050  m1expcl  14051  wrdlen2i  14908  gcdcllem3  16471  lcmfpr  16597  mreincl  17560  acsfn2  17624  ipole  18493  pmtr3ncom  19405  subrngin  20470  subrgin  20505  lssincl  20871  lspvadd  21003  cnmsgnbas  21487  cnmsgngrp  21488  psgninv  21491  zrhpsgnmhm  21493  mdetunilem7  22505  unopn  22790  incld  22930  indiscld  22978  leordtval2  23099  ovolioo  25469  i1f1  25591  aannenlem2  26237  upgrbi  29020  umgrbi  29028  frgr3vlem2  30203  4cycl2v2nb  30218  sshjval3  31283  pr01ssre  32749  psgnid  33054  pmtrto1cl  33056  cnmsgn0g  33103  altgnsg  33106  constrsscn  33730  constrextdg2  33739  mdetpmtr1  33813  mdetpmtr12  33815  esumsnf  34054  prsiga  34121  difelsiga  34123  measssd  34205  carsgsigalem  34306  carsgclctun  34312  pmeasmono  34315  eulerpartlemgs2  34371  eulerpartlemn  34372  probun  34410  signswch  34552  signsvfn  34573  signlem0  34578  breprexpnat  34625  kur14lem1  35193  ssoninhaus  36436  poimirlem15  37629  inidl  38024  pmapmeet  39767  diameetN  41050  dihmeetcN  41296  dihmeet  41337  dvh4dimlem  41437  dvhdimlem  41438  dvh4dimN  41441  dvh3dim3N  41443  lcfrlem23  41559  lcfrlem25  41561  lcfrlem35  41571  mapdindp2  41715  lspindp5  41764  brfvrcld  43680  corclrcl  43696  corcltrcl  43728  ibliooicc  45969  fourierdlem51  46155  fourierdlem64  46168  fourierdlem102  46206  fourierdlem114  46218  sge0sn  46377  ovnsubadd2lem  46643  sprvalpw  47481  prprvalpw  47516  perfectALTVlem2  47723  nnsum3primesgbe  47793  clnbgredg  47840  uhgrimprop  47892  isuspgrimlem  47895  isubgr3stgrlem7  47971  usgrexmpl1lem  48012  usgrexmpl2lem  48017  usgrexmpl2nb1  48023  usgrexmpl2nb2  48024  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  pgnbgreunbgr  48115  fprmappr  48333  zlmodzxzel  48343  zlmodzxzldeplem1  48489  2arymaptfo  48643  prelrrx2  48702  line2x  48743  line2y  48744  onsetreclem2  49695