Description: Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | frege55lem1c | |- ( ( ph -> [. A / x ]. x = B ) -> ( ph -> A = B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-sbc | |- ( [. A / x ]. x = B <-> A e. { x | x = B } ) |
|
2 | eqeq1 | |- ( x = A -> ( x = B <-> A = B ) ) |
|
3 | 2 | elabg | |- ( A e. { x | x = B } -> ( A e. { x | x = B } <-> A = B ) ) |
4 | 3 | ibi | |- ( A e. { x | x = B } -> A = B ) |
5 | 1 4 | sylbi | |- ( [. A / x ]. x = B -> A = B ) |
6 | 5 | imim2i | |- ( ( ph -> [. A / x ]. x = B ) -> ( ph -> A = B ) ) |