Metamath Proof Explorer

Theorem rp-unirabeq

Description: Equality theorem for infimum of non-empty classes of ordinals. (Contributed by RP, 23-Jan-2025)

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

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

Step

Hyp

Ref

Expression

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

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

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