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 397   ∈ wcel 2107   ⊆ wss 3949  {cpr 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-sn 4630  df-pr 4632

This theorem is referenced by:  prssd  4826  tpssi  4840  fr2nr  5655  fprb  7195  f1ofvswap  7304  ordunel  7815  rex2dom  9246  1sdomOLD  9249  dfac2b  10125  tskpr  10765  m1expcl2  14051  m1expcl  14052  wrdlen2i  14893  gcdcllem3  16442  lcmfpr  16564  mreincl  17543  acsfn2  17607  ipole  18487  pmtr3ncom  19343  subrgin  20343  lssincl  20576  lspvadd  20707  cnmsgnbas  21131  cnmsgngrp  21132  psgninv  21135  zrhpsgnmhm  21137  mdetunilem7  22120  unopn  22405  incld  22547  indiscld  22595  leordtval2  22716  ovolioo  25085  i1f1  25207  aannenlem2  25842  upgrbi  28353  umgrbi  28361  frgr3vlem2  29527  4cycl2v2nb  29542  sshjval3  30607  pr01ssre  32030  psgnid  32256  pmtrto1cl  32258  cnmsgn0g  32305  altgnsg  32308  mdetpmtr1  32803  mdetpmtr12  32805  esumsnf  33062  prsiga  33129  difelsiga  33131  measssd  33213  carsgsigalem  33314  carsgclctun  33320  pmeasmono  33323  eulerpartlemgs2  33379  eulerpartlemn  33380  probun  33418  signswch  33572  signsvfn  33593  signlem0  33598  breprexpnat  33646  kur14lem1  34197  ssoninhaus  35333  poimirlem15  36503  inidl  36898  pmapmeet  38644  diameetN  39927  dihmeetcN  40173  dihmeet  40214  dvh4dimlem  40314  dvhdimlem  40315  dvh4dimN  40318  dvh3dim3N  40320  lcfrlem23  40436  lcfrlem25  40438  lcfrlem35  40448  mapdindp2  40592  lspindp5  40641  brfvrcld  42442  corclrcl  42458  corcltrcl  42490  ibliooicc  44687  fourierdlem51  44873  fourierdlem64  44886  fourierdlem102  44924  fourierdlem114  44936  sge0sn  45095  ovnsubadd2lem  45361  sprvalpw  46148  prprvalpw  46183  perfectALTVlem2  46390  nnsum3primesgbe  46460  subrngin  46740  fprmappr  47021  zlmodzxzel  47031  zlmodzxzldeplem1  47181  2arymaptfo  47340  prelrrx2  47399  line2x  47440  line2y  47441  onsetreclem2  47751