Description: Proof of ax-9 from ax9v1 and ax9v2 , proving sufficiency of the conjunction of the latter two weakened versions of ax9v , which is itself a weakened version of ax-9 . (Contributed by BJ, 7-Dec-2020) (Proof shortened by Wolf Lammen, 11-Apr-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax9 | |- ( x = y -> ( z e. x -> z e. y ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | equvinv | |- ( x = y <-> E. t ( t = x /\ t = y ) ) |
|
| 2 | ax9v2 | |- ( x = t -> ( z e. x -> z e. t ) ) |
|
| 3 | 2 | equcoms | |- ( t = x -> ( z e. x -> z e. t ) ) |
| 4 | ax9v1 | |- ( t = y -> ( z e. t -> z e. y ) ) |
|
| 5 | 3 4 | sylan9 | |- ( ( t = x /\ t = y ) -> ( z e. x -> z e. y ) ) |
| 6 | 5 | exlimiv | |- ( E. t ( t = x /\ t = y ) -> ( z e. x -> z e. y ) ) |
| 7 | 1 6 | sylbi | |- ( x = y -> ( z e. x -> z e. y ) ) |