Description: A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993) Avoid ax-12 . (Revised by SN, 8-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ceqsalv.1 | |- A e. _V |
|
ceqsalv.2 | |- ( x = A -> ( ph <-> ps ) ) |
||
Assertion | ceqsalv | |- ( A. x ( x = A -> ph ) <-> ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ceqsalv.1 | |- A e. _V |
|
2 | ceqsalv.2 | |- ( x = A -> ( ph <-> ps ) ) |
|
3 | 19.23v | |- ( A. x ( x = A -> ps ) <-> ( E. x x = A -> ps ) ) |
|
4 | 2 | pm5.74i | |- ( ( x = A -> ph ) <-> ( x = A -> ps ) ) |
5 | 4 | albii | |- ( A. x ( x = A -> ph ) <-> A. x ( x = A -> ps ) ) |
6 | 1 | isseti | |- E. x x = A |
7 | 6 | a1bi | |- ( ps <-> ( E. x x = A -> ps ) ) |
8 | 3 5 7 | 3bitr4i | |- ( A. x ( x = A -> ph ) <-> ps ) |