Theorem coeq1 3287

Description: Equality theorem for composition of two classes.

Assertion

Ref	Expression
coeq1	|- (A = B -> (A o. C) = (B o. C))

Proof of Theorem coeq1

Step	Hyp	Ref	Expression
1		breq 2626	. . . . 5 |- (A = B -> (zAy <-> zBy))
2	1	anbi2d 618	. . . 4 |- (A = B -> ((xCz /\ zAy) <-> (xCz /\ zBy)))
3	2	exbidv 1281	. . 3 |- (A = B -> (E.z(xCz /\ zAy) <-> E.z(xCz /\ zBy)))
4	3	opabbidv 2675	. 2 |- (A = B -> {<.x, y>. | E.z(xCz /\ zAy)} = {<.x, y>. | E.z(xCz /\ zBy)})
5		df-co 3193	. 2 |- (A o. C) = {<.x, y>. | E.z(xCz /\ zAy)}
6		df-co 3193	. 2 |- (B o. C) = {<.x, y>. | E.z(xCz /\ zBy)}
7	4, 5, 6	3eqtr4g 1534	1 |- (A = B -> (A o. C) = (B o. C))

Syntax hints:   -> wi 3   /\ wa 223   = wceq 958  E.wex 982   class class class wbr 2624  {copab 2671   o. ccom 3180

This theorem is referenced by:  coeq1i 3289  coeq1d 3291  coi2 3517  ereq 4273  isps 8641  hocsubdirt 9706  hoddit 9910  hmopidmcht 10076  hmopidmpjt 10077  pjidmcot 10104  pjhmopidm 10105  dfpjopt 10106  symgoprval 10399  hmeogrp 10524

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-br 2625  df-opab 2672  df-co 3193

Copyright terms: Public domain