Metamath Proof Explorer


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 y A x = y y B x = y
2 1 abbidv A = B x | y A x = y = x | y B x = y
3 df-bj-sngl sngl A = x | y A x = y
4 df-bj-sngl sngl B = x | y B x = y
5 2 3 4 3eqtr4g A = B sngl A = sngl B