Theorem prssi 4752

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119   ⊆ wss 3883  {cpr 4557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-ss 3900  df-sn 4556  df-pr 4558

This theorem is referenced by:  prssd  4753  tpssi  4769  fr2nr  5595  fprb  7138  f1ofvswap  7250  ordunel  7767  rex2dom  9153  dfac2b  10044  tskpr  10684  pr01ssre  11139  m1expcl2  14038  m1expcl  14039  wrdlen2i  14895  gcdcllem3  16461  lcmfpr  16587  mreincl  17552  acsfn2  17620  ipole  18491  pmtr3ncom  19441  subrngin  20533  subrgin  20568  lssincl  20955  lspvadd  21086  cnmsgnbas  21553  cnmsgngrp  21554  psgninv  21557  zrhpsgnmhm  21559  mdetunilem7  22601  unopn  22886  incld  23026  indiscld  23074  leordtval2  23195  ovolioo  25553  i1f1  25675  aannenlem2  26313  upgrbi  29180  umgrbi  29188  frgr3vlem2  30362  4cycl2v2nb  30377  sshjval3  31443  psgnid  33178  pmtrto1cl  33180  cnmsgn0g  33227  altgnsg  33230  constrsscn  33924  constrextdg2  33933  mdetpmtr1  34007  mdetpmtr12  34009  esumsnf  34248  prsiga  34315  difelsiga  34317  measssd  34399  carsgsigalem  34499  carsgclctun  34505  pmeasmono  34508  eulerpartlemgs2  34564  eulerpartlemn  34565  probun  34603  signswch  34745  signsvfn  34766  signlem0  34771  breprexpnat  34818  kur14lem1  35434  ssoninhaus  36676  poimirlem15  38002  inidl  38397  pmapmeet  40265  diameetN  41548  dihmeetcN  41794  dihmeet  41835  dvh4dimlem  41935  dvhdimlem  41936  dvh4dimN  41939  dvh3dim3N  41941  lcfrlem23  42057  lcfrlem25  42059  lcfrlem35  42069  mapdindp2  42213  lspindp5  42262  brfvrcld  44135  corclrcl  44151  corcltrcl  44183  ibliooicc  46414  fourierdlem51  46600  fourierdlem64  46613  fourierdlem102  46651  fourierdlem114  46663  sge0sn  46822  ovnsubadd2lem  47088  sprvalpw  47955  prprvalpw  47990  perfectALTVlem2  48213  nnsum3primesgbe  48283  clnbgredg  48331  uhgrimprop  48383  isuspgrimlem  48386  isubgr3stgrlem7  48463  usgrexmpl1lem  48512  usgrexmpl2lem  48517  usgrexmpl2nb1  48523  usgrexmpl2nb2  48524  usgrexmpl2nb4  48526  usgrexmpl2nb5  48527  pgnbgreunbgr  48616  fprmappr  48836  zlmodzxzel  48846  zlmodzxzldeplem1  48991  2arymaptfo  49145  prelrrx2  49204  line2x  49245  line2y  49246  onsetreclem2  50196