Theorem bj-sngleq

Description: Substitution property for sngl . (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-sngleq	|- ( A = B -> sngl A = sngl B )

Proof

Step	Hyp	Ref	Expression
1		rexeq	|- ( A = B -> ( E. y e. A x = { y } <-> E. y e. B x = { y } ) )
2	1	abbidv	|- ( A = B -> { x | E. y e. A x = { y } } = { x | E. y e. B x = { y } } )
3		df-bj-sngl	|- sngl A = { x | E. y e. A x = { y } }
4		df-bj-sngl	|- sngl B = { x | E. y e. B x = { y } }
5	2 3 4	3eqtr4g	|- ( A = B -> sngl A = sngl B )