Theorem prssi 4782

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   ⊆ wss 3899  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916  df-sn 4585  df-pr 4587

This theorem is used by:  prssd  4783  tpssi  4798  fr2nr  5632  fprb  7193  f1ofvswap  7308  ordunel  7824  rex2dom  9226  dfac2b  10136  tskpr  10782  pr01ssre  11239  m1expcl2  14152  m1expcl  14153  wrdlen2i  15016  gcdcllem3  16594  lcmfpr  16720  mreincl  17686  acsfn2  17754  ipole  18625  pmtr3ncom  19605  subrngin  20726  subrgin  20761  lssincl  21152  lspvadd  21283  cnmsgnbas  21794  cnmsgngrp  21795  psgninv  21798  zrhpsgnmhm  21800  mdetunilem7  22843  unopn  23131  incld  23271  indiscld  23319  leordtval2  23440  ovolioo  25799  i1f1  25921  aannenlem2  26568  upgrbi  29553  umgrbi  29561  frgr3vlem2  30757  4cycl2v2nb  30772  sshjval3  31838  psgnid  33540  pmtrto1cl  33542  cnmsgn0g  33589  altgnsg  33592  inlidl  33852  constrsscn  34253  constrextdg2  34262  mdetpmtr1  34336  mdetpmtr12  34338  esumsnf  34577  prsiga  34644  measssd  34729  carsgsigalem  34829  carsgclctun  34835  pmeasmono  34838  eulerpartlemgs2  34894  eulerpartlemn  34895  probun  34933  signswch  35072  signsvfn  35093  signlem0  35098  breprexpnat  35145  kur14lem1  35788  ssoninhaus  37070  poimirlem15  38387  inidl  38783  pmapmeet  40649  diameetN  41932  dihmeetcN  42178  dihmeet  42219  dvh4dimlem  42319  dvhdimlem  42320  dvh4dimN  42323  dvh3dim3N  42325  lcfrlem23  42441  lcfrlem25  42443  lcfrlem35  42453  mapdindp2  42597  lspindp5  42646  brfvrcld  44534  corclrcl  44550  corcltrcl  44582  ibliooicc  46802  fourierdlem51  46988  fourierdlem64  47001  fourierdlem102  47039  fourierdlem114  47051  sge0sn  47210  ovnsubadd2lem  47476  sprvalpw  48383  prprvalpw  48418  perfectALTVlem2  48641  nnsum3primesgbe  48711  clnbgredg  48759  uhgrimprop  48811  isuspgrimlem  48814  isubgr3stgrlem7  48891  usgrexmpl1lem  48940  usgrexmpl2lem  48945  usgrexmpl2nb1  48951  usgrexmpl2nb2  48952  usgrexmpl2nb4  48954  usgrexmpl2nb5  48955  pgnbgreunbgr  49044  fprmappr  49278  zlmodzxzel  49288  zlmodzxzldeplem1  49433  2arymaptfo  49587  prelrrx2  49646  line2x  49687  line2y  49688  onsetreclem2  50635