Theorem eceq1 6548

Description: Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)

Assertion

Ref	Expression
eceq1	|- ( A = B -> [ A ] C = [ B ] C )

Proof of Theorem eceq1

Step	Hyp	Ref	Expression
1		sneq 3594	. . 3 |- ( A = B -> { A } = { B } )
2	1	imaeq2d 4953	. 2 |- ( A = B -> ( C " { A } ) = ( C " { B } ) )
3		df-ec 6515	. 2 |- [ A ] C = ( C " { A } )
4		df-ec 6515	. 2 |- [ B ] C = ( C " { B } )
5	2, 3, 4	3eqtr4g 2228	1 |- ( A = B -> [ A ] C = [ B ] C )

Syntax hints:   -> wi 4   = wceq 1348   {csn 3583   "cima 4614   [cec 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-sn 3589  df-pr 3590  df-op 3592  df-br 3990  df-opab 4051  df-xp 4617  df-cnv 4619  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-ec 6515

This theorem is referenced by:  eceq1d  6549  ecelqsg  6566  snec  6574  qliftfun  6595  qliftfuns  6597  qliftval  6599  ecoptocl  6600  eroveu  6604  th3qlem1  6615  th3qlem2  6616  th3q  6618  dmaddpqlem  7339  nqpi  7340  1qec  7350  nqnq0  7403  nq0nn  7404  mulnnnq0  7412  addpinq1  7426  caucvgsrlemfv  7753  caucvgsr  7764  pitonnlem1  7807  axcaucvg  7862