Theorem supeq1 4575

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 1786	. . . . 5 |- (B = C -> (A.y e. B -. xRy <-> A.y e. C -. xRy))
2		rexeq1 1787	. . . . . . 7 |- (B = C -> (E.z e. B yRz <-> E.z e. C yRz))
3	2	imbi2d 612	. . . . . 6 |- (B = C -> ((yRx -> E.z e. B yRz) <-> (yRx -> E.z e. C yRz)))
4	3	ralbidv 1663	. . . . 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 628	. . . 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 1807	. . 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 2512	. 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 4574	. 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 4574	. 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 1531	1 |- (B = C -> sup(B, A, R) = sup(C, A, R))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 223   = wceq 956  A.wral 1645  E.wrex 1646  {crab 1648  U.cuni 2503   class class class wbr 2619  supcsup 4573

This theorem is referenced by:  supsn 4591  supxrmnf 6087  nninfm 6463  nn0infm 6464  limsupvalt 6529  sqrval 6671  sqr0 6672  isupivth 7290  metxpdval 7829  nmofval 8425  nmoval 8426  nmo0 8451  pilem3 8673  pilem4 8674  nmopvalt 9782  nmfnvalt 9803  nmopneg 9889  nmop0 9910  nmfn0 9911  nmcopex 9957  nmcfnex 9986  ee7.2a 10425

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ral 1649  df-rex 1650  df-rab 1652  df-uni 2504  df-sup 4574

Copyright terms: Public domain