Metamath Proof Explorer

Theorem rp-intrabeq

Description: Equality theorem for supremum of sets of ordinals. (Contributed by RP, 23-Jan-2025)

		Ref	Expression
	Assertion	rp-intrabeq	\|- ( A = B -> \|^\| { x e. On \| A. y e. A y C_ x } = \|^\| { x e. On \| A. y e. B y C_ x } )

Step	Hyp	Ref	Expression
1		raleq	\|- ( A = B -> ( A. y e. A y C_ x <-> A. y e. B y C_ x ) )
2	1	rabbidv	\|- ( A = B -> { x e. On \| A. y e. A y C_ x } = { x e. On \| A. y e. B y C_ x } )
3	2	inteqd	\|- ( A = B -> \|^\| { x e. On \| A. y e. A y C_ x } = \|^\| { x e. On \| A. y e. B y C_ x } )

Step

Hyp

Ref

Expression

 |-  ( A = B -> ( A. y e. A y C_ x <-> A. y e. B y C_ x ) )

 |-  ( A = B -> { x e. On | A. y e. A y C_ x } = { x e. On | A. y e. B y C_ x } )

 |-  ( A = B -> |^| { x e. On | A. y e. A y C_ x } = |^| { x e. On | A. y e. B y C_ x } )