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 df-clab . (Revised by Wolf Lammen, 23-Jan-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ceqsal.1 | |- F/ x ps |
|
ceqsal.2 | |- A e. _V |
||
ceqsal.3 | |- ( x = A -> ( ph <-> ps ) ) |
||
Assertion | ceqsal | |- ( A. x ( x = A -> ph ) <-> ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ceqsal.1 | |- F/ x ps |
|
2 | ceqsal.2 | |- A e. _V |
|
3 | ceqsal.3 | |- ( x = A -> ( ph <-> ps ) ) |
|
4 | 1 | 19.23 | |- ( A. x ( x = A -> ps ) <-> ( E. x x = A -> ps ) ) |
5 | 3 | pm5.74i | |- ( ( x = A -> ph ) <-> ( x = A -> ps ) ) |
6 | 5 | albii | |- ( A. x ( x = A -> ph ) <-> A. x ( x = A -> ps ) ) |
7 | 2 | isseti | |- E. x x = A |
8 | 7 | a1bi | |- ( ps <-> ( E. x x = A -> ps ) ) |
9 | 4 6 8 | 3bitr4i | |- ( A. x ( x = A -> ph ) <-> ps ) |