Theorem supeq1 4549

Description: Equality theorem for supremum.

Assertion

Ref	Expression
supeq1	|- (B = C -> sup(B, A, R) = sup(C, A, R))

Proof of Theorem supeq1

Step	Hyp	Ref	Expression
1		raleq1 1778	. . . . 5 |- (B = C -> (A.y e. B -. xRy <-> A.y e. C -. xRy))
2		rexeq1 1779	. . . . . . 7 |- (B = C -> (E.z e. B yRz <-> E.z e. C yRz))
3	2	imbi2d 610	. . . . . 6 |- (B = C -> ((yRx -> E.z e. B yRz) <-> (yRx -> E.z e. C yRz)))
4	3	ralbidv 1655	. . . . 5 |- (B = C -> (A.y e. A (yRx -> E.z e. B yRz) <-> A.y e. A (yRx -> E.z e. C yRz)))
5	1, 4	anbi12d 626	. . . 4 |- (B = C -> ((A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz)) <-> (A.y e. C -. xRy /\ A.y e. A (yRx -> E.z e. C yRz))))
6	5	rabbisdv 1798	. . 3 |- (B = C -> {x e. A | (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))} = {x e. A | (A.y e. C -. xRy /\ A.y e. A (yRx -> E.z e. C yRz))})
7	6	unieqd 2502	. 2 |- (B = C -> U.{x e. A | (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))} = U.{x e. A | (A.y e. C -. xRy /\ A.y e. A (yRx -> E.z e. C yRz))})
8		df-sup 4548	. 2 |- sup(B, A, R) = U.{x e. A | (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))}
9		df-sup 4548	. 2 |- sup(C, A, R) = U.{x e. A | (A.y e. C -. xRy /\ A.y e. A (yRx -> E.z e. C yRz))}
10	7, 8, 9	3eqtr4g 1523	1 |- (B = C -> sup(B, A, R) = sup(C, A, R))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 223   = wceq 953  A.wral 1637  E.wrex 1638  {crab 1640  U.cuni 2493   class class class wbr 2609  supcsup 4547

This theorem is referenced by:  supsn 4563  supxrmnf 6034  nninfm 6395  nn0infm 6396  limsupvalt 6461  sqrval 6601  sqr0 6602  isupivth 7225  ivth2OLD 7234  metxpdval 7769  nmofval 8357  nmoval 8358  nmo0 8383  pilem3 8592  pilem4 8593  nmopvalt 9699  nmfnvalt 9720  nmopneg 9805  nmop0 9826  nmfn0 9827  nmcopex 9872  nmcfnex 9901

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-ral 1641  df-rex 1642  df-rab 1644  df-uni 2494  df-sup 4548

Copyright terms: Public domain