Description: An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . See equsalhw for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 2-Jun-1993) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | equsalh.1 | |- ( ps -> A. x ps ) |
|
equsalh.2 | |- ( x = y -> ( ph <-> ps ) ) |
||
Assertion | equsalh | |- ( A. x ( x = y -> ph ) <-> ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equsalh.1 | |- ( ps -> A. x ps ) |
|
2 | equsalh.2 | |- ( x = y -> ( ph <-> ps ) ) |
|
3 | 1 | nf5i | |- F/ x ps |
4 | 3 2 | equsal | |- ( A. x ( x = y -> ph ) <-> ps ) |