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

Theorem preq1 4064
Description: Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.)
Assertion
Ref Expression
preq1  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)

Proof of Theorem preq1
StepHypRef Expression
1 sneq 3990 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
21uneq1d 3599 . 2  |-  ( A  =  B  ->  ( { A }  u.  { C } )  =  ( { B }  u.  { C } ) )
3 df-pr 3983 . 2  |-  { A ,  C }  =  ( { A }  u.  { C } )
4 df-pr 3983 . 2  |-  { B ,  C }  =  ( { B }  u.  { C } )
52, 3, 43eqtr4g 2521 1  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455    u. cun 3414   {csn 3980   {cpr 3982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-un 3421  df-sn 3981  df-pr 3983
This theorem is referenced by:  preq2  4065  preq12  4066  preq1i  4067  preq1d  4070  tpeq1  4073  prnzg  4105  preq1b  4159  preq12b  4164  preq12bg  4168  prel12g  4169  elpreqpr  4175  opeq1  4180  uniprg  4226  intprg  4283  prex  4656  fprg  6097  fnpr2g  6149  opthreg  8149  brdom7disj  8985  brdom6disj  8986  wunpr  9160  wunex2  9189  wuncval2  9198  grupr  9248  wwlktovf  13080  joindef  16299  meetdef  16313  pptbas  20072  usgraedg4  25163  usgraidx2vlem2  25168  usgraidx2v  25169  nbgraop  25200  nb3graprlem2  25229  cusgrarn  25236  cusgra2v  25239  nbcusgra  25240  cusgra3v  25241  cusgrafilem2  25257  usgrasscusgra  25260  uvtxnbgra  25270  usgra2wlkspthlem1  25396  usgrcyclnl2  25418  4cycl4dv  25444  usg2spthonot0  25666  rusgraprop4  25721  rusgrasn  25722  rusgranumwwlkl1  25723  rusgranumwlks  25733  frgra2v  25776  frgra3vlem1  25777  frgra3vlem2  25778  3vfriswmgra  25782  3cyclfrgrarn1  25789  4cycl2vnunb  25794  vdn0frgrav2  25800  vdgn0frgrav2  25801  vdn1frgrav2  25802  vdgn1frgrav2  25803  frgrancvvdeqlemB  25815  frgrancvvdeqlemC  25816  frgrawopreglem5  25825  frgrawopreg1  25827  frgraregorufr0  25829  frg2woteqm  25836  usg2spot2nb  25842  extwwlkfablem1  25851  altopthsn  30777  hdmap11lem2  35458  sge0prle  38281  meadjun  38338  propeqop  39039  elpr2elpr  39043  upgredg  39276  usgredg4  39344  usgredg2vlem2  39353  usgredg2v  39354  nbgrval  39456  nb3grprlem2  39505  cusgredg  39542  cusgrfilem2  39567  usgredgsscusgredg  39570  upgr3v3e3cycl  39921  upgr4cycl4dv4e  39926  usgvincvad  39989  usgvincvadALT  39992  usgedgvadf1lem2  39999  usgedgvadf1  40000  usgedgvadf1ALTlem2  40002  usgedgvadf1ALT  40003
  Copyright terms: Public domain W3C validator