Theorem eceq1 6665

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

Assertion

Ref	Expression
eceq1	⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)

Proof of Theorem eceq1

Step	Hyp	Ref	Expression
1		sneq 3646	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	imaeq2d 5028	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 “ {𝐴}) = (𝐶 “ {𝐵}))
3		df-ec 6632	. 2 ⊢ [𝐴]𝐶 = (𝐶 “ {𝐴})
4		df-ec 6632	. 2 ⊢ [𝐵]𝐶 = (𝐶 “ {𝐵})
5	2, 3, 4	3eqtr4g 2264	1 ⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)

Syntax hints:   → wi 4   = wceq 1373  {csn 3635   “ cima 4683  [cec 6628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3172  df-in 3174  df-ss 3181  df-sn 3641  df-pr 3642  df-op 3644  df-br 4049  df-opab 4111  df-xp 4686  df-cnv 4688  df-dm 4690  df-rn 4691  df-res 4692  df-ima 4693  df-ec 6632

This theorem is referenced by:  eceq1d  6666  ecelqsg  6685  snec  6693  qliftfun  6714  qliftfuns  6716  qliftval  6718  ecoptocl  6719  eroveu  6723  th3qlem1  6734  th3qlem2  6735  th3q  6737  dmaddpqlem  7503  nqpi  7504  1qec  7514  nqnq0  7567  nq0nn  7568  mulnnnq0  7576  addpinq1  7590  caucvgsrlemfv  7917  caucvgsr  7928  pitonnlem1  7971  axcaucvg  8026  divsfval  13210  divsfvalg  13211  qusghm  13668  znzrhval  14459