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

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

Proof of Theorem preq1
StepHypRef Expression
1 sneq 4220 . . 3 (𝐴 = 𝐵 → {𝐴} = {𝐵})
21uneq1d 3799 . 2 (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶}))
3 df-pr 4213 . 2 {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
4 df-pr 4213 . 2 {𝐵, 𝐶} = ({𝐵} ∪ {𝐶})
52, 3, 43eqtr4g 2710 1 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1523   ∪ cun 3605  {csn 4210  {cpr 4212 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-sn 4211  df-pr 4213 This theorem is referenced by:  preq2  4301  preq12  4302  preq1i  4303  preq1d  4306  tpeq1  4309  prnzgOLD  4343  preq1b  4409  preq12b  4413  preq12bg  4417  prel12g  4418  elpreqpr  4427  elpr2elpr  4429  opeq1  4433  uniprg  4482  intprg  4543  prex  4939  propeqop  4999  fprg  6462  fnpr2g  6515  opthreg  8553  brdom7disj  9391  brdom6disj  9392  wunpr  9569  wunex2  9598  wuncval2  9607  grupr  9657  wwlktovf  13745  joindef  17051  meetdef  17065  pptbas  20860  usgredg4  26154  usgredg2vlem2  26163  usgredg2v  26164  nbgrval  26274  nb3grprlem2  26327  cusgredg  26376  cusgrfilem2  26408  usgredgsscusgredg  26411  rusgrnumwrdl2  26538  usgr2trlncl  26712  crctcshwlkn0lem6  26763  rusgrnumwwlks  26941  upgr3v3e3cycl  27158  upgr4cycl4dv4e  27163  eupth2lem3lem4  27209  nfrgr2v  27252  frgr3vlem1  27253  frgr3vlem2  27254  3vfriswmgr  27258  3cyclfrgrrn1  27265  4cycl2vnunb  27270  vdgn1frgrv2  27276  frgrncvvdeqlem8  27286  frgrncvvdeqlem9  27287  frgrwopregasn  27296  frgrwopreglem5ALT  27302  extwwlkfablem1OLD  27323  2clwwlk2clwwlklem2lem2  27329  altopthsn  32193  hdmap11lem2  37451  sge0prle  40936  meadjun  40997  elsprel  42050  prelspr  42061  sprsymrelfolem2  42068
 Copyright terms: Public domain W3C validator