Theorem coeq1 3276

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 2616	. . . . 5 |- (A = B -> (zAy <-> zBy))
2	1	anbi2d 615	. . . 4 |- (A = B -> ((xCz /\ zAy) <-> (xCz /\ zBy)))
3	2	exbidv 1277	. . 3 |- (A = B -> (E.z(xCz /\ zAy) <-> E.z(xCz /\ zBy)))
4	3	opabbidv 2665	. 2 |- (A = B -> {<.x, y>. | E.z(xCz /\ zAy)} = {<.x, y>. | E.z(xCz /\ zBy)})
5		df-co 3182	. 2 |- (A o. C) = {<.x, y>. | E.z(xCz /\ zAy)}
6		df-co 3182	. 2 |- (B o. C) = {<.x, y>. | E.z(xCz /\ zBy)}
7	4, 5, 6	3eqtr4g 1528	1 |- (A = B -> (A o. C) = (B o. C))

Syntax hints:   -> wi 3   /\ wa 223   = wceq 954  E.wex 978   class class class wbr 2614  {copab 2661   o. ccom 3169

This theorem is referenced by:  coeq1i 3278  coeq1d 3280  coi2 3503  ereq 4257  isps 8588  hocsubdirt 9651  hoddit 9853  hmopidmcht 10019  hmopidmpjt 10020  pjidmcot 10047  pjhmopidm 10048  dfpjopt 10049  symgoprval 10338  hmeogrp 10461

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-br 2615  df-opab 2662  df-co 3182

Copyright terms: Public domain