Metamath Proof Explorer

Theorem sbab

Description: The right-hand side of the second equality is a way of representing proper substitution of y for x into a class variable. (Contributed by NM, 14-Sep-2003)

Ref Expression
Assertion sbab x = y A = z | y x z A


Step Hyp Ref Expression
1 sbequ12 x = y z A y x z A
2 1 abbi2dv x = y A = z | y x z A