MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  preq1 Structured version   Visualization version   GIF version

Theorem preq1 4470
Description: Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.)
Assertion
Ref Expression
preq1 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})

Proof of Theorem preq1
StepHypRef Expression
1 sneq 4391 . . 3 (𝐴 = 𝐵 → {𝐴} = {𝐵})
21uneq1d 3976 . 2 (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3 df-pr 4384 . 2 {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4 df-pr 4384 . 2 {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
52, 3, 43eqtr4g 2876 1 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  cun 3778  {csn 4381  {cpr 4383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-v 3404  df-un 3785  df-sn 4382  df-pr 4384
This theorem is referenced by:  preq2  4471  preq12  4472  preq1i  4473  preq1d  4476  tpeq1  4479  preq1b  4576  preq12b  4580  preq12bg  4584  prel12gOLD  4585  prel12g  4597  elpreqpr  4600  elpr2elpr  4602  opeq1  4606  uniprg  4655  intprg  4714  prex  5112  propeqop  5175  opthhausdorff  5185  opthhausdorff0  5186  fprg  6656  fnpr2g  6709  opthreg  8770  opthregOLD  8772  brdom7disj  9648  brdom6disj  9649  wunpr  9826  wunex2  9855  wuncval2  9864  grupr  9914  wwlktovf  13944  joindef  17229  meetdef  17243  pptbas  21047  usgredg4  26347  usgredg2vlem2  26356  usgredg2v  26357  nbgrval  26468  nb3grprlem2  26522  cusgredg  26571  cusgrfilem2  26603  usgredgsscusgredg  26606  rusgrnumwrdl2  26733  usgr2trlncl  26907  crctcshwlkn0lem6  26959  rusgrnumwwlks  27139  upgr3v3e3cycl  27376  upgr4cycl4dv4e  27381  eupth2lem3lem4  27427  nfrgr2v  27470  frgr3vlem1  27471  frgr3vlem2  27472  3vfriswmgr  27476  3cyclfrgrrn1  27483  4cycl2vnunb  27488  vdgn1frgrv2  27494  frgrncvvdeqlem8  27504  frgrncvvdeqlem9  27505  frgrwopregasn  27514  frgrwopreglem5ALT  27520  extwwlkfablem1OLD  27540  2clwwlk2clwwlklem  27546  altopthsn  32411  hdmap11lem2  37641  sge0prle  41115  meadjun  41176  elsprel  42311  prelspr  42322  sprsymrelfolem2  42329
  Copyright terms: Public domain W3C validator