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 | |- ( [ y / x ] A e. B <-> [_ y / x ]_ A e. B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbsbc | |- ( [ y / x ] A e. B <-> [. y / x ]. A e. B ) |
|
2 | sbcel1g | |- ( y e. _V -> ( [. y / x ]. A e. B <-> [_ y / x ]_ A e. B ) ) |
|
3 | 2 | elv | |- ( [. y / x ]. A e. B <-> [_ y / x ]_ A e. B ) |
4 | 1 3 | bitri | |- ( [ y / x ] A e. B <-> [_ y / x ]_ A e. B ) |