Theorem supeq1 4584

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 1789	. . . . 5 |- (B = C -> (A.y e. B -. xRy <-> A.y e. C -. xRy))
2		rexeq1 1790	. . . . . . 7 |- (B = C -> (E.z e. B yRz <-> E.z e. C yRz))
3	2	imbi2d 614	. . . . . 6 |- (B = C -> ((yRx -> E.z e. B yRz) <-> (yRx -> E.z e. C yRz)))
4	3	ralbidv 1666	. . . . 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 630	. . . 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 1810	. . 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 2516	. 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 4583	. 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 4583	. 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 1534	1 |- (B = C -> sup(B, A, R) = sup(C, A, R))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 223   = wceq 958  A.wral 1648  E.wrex 1649  {crab 1651  U.cuni 2507   class class class wbr 2624  supcsup 4582

This theorem is referenced by:  supsn 4600  supxrmnf 6089  nninfm 6464  nn0infm 6465  limsupvalt 6530  sqrval 6672  sqr0 6673  isupivth 7290  metxpdval 7826  nmofval 8421  nmoval 8422  nmo0 8447  pilem3 8668  pilem4 8669  nmopvalt 9777  nmfnvalt 9798  nmopneg 9884  nmop0 9905  nmfn0 9906  nmcopex 9952  nmcfnex 9981  ee7.2a 10420

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-ral 1652  df-rex 1653  df-rab 1655  df-uni 2508  df-sup 4583

Copyright terms: Public domain