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