Theorem ax8 1904

Description: Proof of ax-8 1900 from ax8v1 1902 and ax8v2 1903, proving sufficiency of the conjunction of the latter two weakened versions of ax8v 1901, which is itself a weakened version of ax-8 1900. (Contributed by BJ, 7-Dec-2020.)

Assertion

Ref	Expression
ax8	|- ( x = y -> ( x e. z -> y e. z ) )

Proof of Theorem ax8

Dummy variable t is distinct from all other variables.

Step	Hyp	Ref	Expression
1		equviniv 1883	. 2 |- ( x = y -> E. t ( x = t /\ y = t ) )
2		equcomiv 1869	. . . . 5 |- ( y = t -> t = y )
3	2	adantl 472	. . . 4 |- ( ( x = t /\ y = t ) -> t = y )
4		ax8v2 1903	. . . . 5 |- ( x = t -> ( x e. z -> t e. z ) )
5	4	adantr 471	. . . 4 |- ( ( x = t /\ y = t ) -> ( x e. z -> t e. z ) )
6		ax8v1 1902	. . . 4 |- ( t = y -> ( t e. z -> y e. z ) )
7	3, 5, 6	sylsyld 58	. . 3 |- ( ( x = t /\ y = t ) -> ( x e. z -> y e. z ) )
8	7	exlimiv 1787	. 2 |- ( E. t ( x = t /\ y = t ) -> ( x e. z -> y e. z ) )
9	1, 8	syl 17	1 |- ( x = y -> ( x e. z -> y e. z ) )

Syntax hints:   -> wi 4   /\ wa 375   E.wex 1674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675

This theorem is referenced by:  elequ1  1905  el  4602  axextdfeq  30494  ax8dfeq  30495  exnel  30499  bj-ax89  31322  bj-el  31457