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

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

Proof of Theorem preq1
StepHypRef Expression
1 sneq 4331 . . 3 (𝐴 = 𝐵 → {𝐴} = {𝐵})
21uneq1d 3909 . 2 (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3 df-pr 4324 . 2 {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4 df-pr 4324 . 2 {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
52, 3, 43eqtr4g 2819 1 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  cun 3713  {csn 4321  {cpr 4323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-un 3720  df-sn 4322  df-pr 4324
This theorem is referenced by:  preq2  4413  preq12  4414  preq1i  4415  preq1d  4418  tpeq1  4421  prnzgOLD  4455  preq1b  4522  preq12b  4526  preq12bg  4530  prel12gOLD  4531  prel12g  4544  elpreqpr  4547  elpr2elpr  4549  opeq1  4553  uniprg  4602  intprg  4663  prex  5058  propeqop  5118  opthhausdorff  5127  opthhausdorff0  5128  fprg  6585  fnpr2g  6638  opthreg  8686  opthregOLD  8688  brdom7disj  9545  brdom6disj  9546  wunpr  9723  wunex2  9752  wuncval2  9761  grupr  9811  wwlktovf  13900  joindef  17205  meetdef  17219  pptbas  21014  usgredg4  26308  usgredg2vlem2  26317  usgredg2v  26318  nbgrval  26428  nb3grprlem2  26481  cusgredg  26530  cusgrfilem2  26562  usgredgsscusgredg  26565  rusgrnumwrdl2  26692  usgr2trlncl  26866  crctcshwlkn0lem6  26918  rusgrnumwwlks  27096  upgr3v3e3cycl  27332  upgr4cycl4dv4e  27337  eupth2lem3lem4  27383  nfrgr2v  27426  frgr3vlem1  27427  frgr3vlem2  27428  3vfriswmgr  27432  3cyclfrgrrn1  27439  4cycl2vnunb  27444  vdgn1frgrv2  27450  frgrncvvdeqlem8  27460  frgrncvvdeqlem9  27461  frgrwopregasn  27470  frgrwopreglem5ALT  27476  extwwlkfablem1OLD  27497  2clwwlk2clwwlklem  27503  altopthsn  32374  hdmap11lem2  37636  sge0prle  41121  meadjun  41182  elsprel  42235  prelspr  42246  sprsymrelfolem2  42253
  Copyright terms: Public domain W3C validator