Metamath Proof Explorer


Theorem bj-sbel1

Description: Version of sbcel1g when substituting a set. (Note: one could have a corresponding version of sbcel12 when substituting a set, but the point here is that the antecedent of sbcel1g is not needed when substituting a set.) (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-sbel1 yxABy/xAB

Proof

Step Hyp Ref Expression
1 sbsbc yxAB[˙y/x]˙AB
2 sbcel1g yV[˙y/x]˙ABy/xAB
3 2 elv [˙y/x]˙ABy/xAB
4 1 3 bitri yxABy/xAB