Theorem preq1 4268

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

Step	Hyp	Ref	Expression
1		sneq 4187	. . 3 |- ( A = B -> { A } = { B } )
2	1	uneq1d 3766	. 2 |- ( A = B -> ( { A } u. { C } ) = ( { B } u. { C } ) )
3		df-pr 4180	. 2 |- { A , C } = ( { A } u. { C } )
4		df-pr 4180	. 2 |- { B , C } = ( { B } u. { C } )
5	2, 3, 4	3eqtr4g 2681	1 |- ( A = B -> { A , C } = { B , C } )

Syntax hints:   -> wi 4   = wceq 1483   u. cun 3572   {csn 4177   {cpr 4179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-sn 4178  df-pr 4180

This theorem is referenced by:  preq2  4269  preq12  4270  preq1i  4271  preq1d  4274  tpeq1  4277  prnzgOLD  4312  preq1b  4377  preq12b  4382  preq12bg  4386  prel12g  4387  elpreqpr  4396  elpr2elpr  4398  opeq1  4402  uniprg  4450  intprg  4511  prex  4909  propeqop  4970  fprg  6422  fnpr2g  6474  opthreg  8515  brdom7disj  9353  brdom6disj  9354  wunpr  9531  wunex2  9560  wuncval2  9569  grupr  9619  wwlktovf  13699  joindef  17004  meetdef  17018  pptbas  20812  usgredg4  26109  usgredg2vlem2  26118  usgredg2v  26119  nbgrval  26234  nb3grprlem2  26283  cusgredg  26320  cusgrfilem2  26352  usgredgsscusgredg  26355  rusgrnumwrdl2  26482  usgr2trlncl  26656  crctcshwlkn0lem6  26707  rusgrnumwwlks  26869  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  eupth2lem3lem4  27091  nfrgr2v  27136  frgr3vlem1  27137  frgr3vlem2  27138  3vfriswmgr  27142  3cyclfrgrrn1  27149  4cycl2vnunb  27154  vdgn1frgrv2  27160  frgrncvvdeqlem8  27170  frgrncvvdeqlem9  27171  frgrwopregasn  27180  frgrwopreglem5ALT  27186  extwwlkfablem1  27207  altopthsn  32068  hdmap11lem2  37134  sge0prle  40618  meadjun  40679  elsprel  41725  prelspr  41736  sprsymrelfolem2  41743