Description: A property related to substitution that unlike equs5 does not require a distinctor antecedent. This proof uses ax12 , see equs5eALT for an alternative one using ax-12 but not ax13 . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 2-Feb-2007) (Proof shortened by Wolf Lammen, 15-Jan-2018) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | equs5e | |- ( E. x ( x = y /\ ph ) -> A. x ( x = y -> E. y ph ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfa1 | |- F/ x A. x ( x = y -> E. y ph ) |
|
2 | ax12 | |- ( x = y -> ( A. y E. y ph -> A. x ( x = y -> E. y ph ) ) ) |
|
3 | hbe1 | |- ( E. y ph -> A. y E. y ph ) |
|
4 | 3 | 19.23bi | |- ( ph -> A. y E. y ph ) |
5 | 2 4 | impel | |- ( ( x = y /\ ph ) -> A. x ( x = y -> E. y ph ) ) |
6 | 1 5 | exlimi | |- ( E. x ( x = y /\ ph ) -> A. x ( x = y -> E. y ph ) ) |