Theorem frege104

Description: Proposition 104 of Frege1879 p. 73.

Note: in the Bauer-Meenfelberg translation published in van Heijenoort's collectionFrom Frege to Goedel, this proof has the minor clause and result swapped. (Contributed by RP, 7-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	frege103.z	|- Z e. V
Assertion	frege104	|- ( X ( ( t+ ` R ) u. _I ) Z -> ( -. X ( t+ ` R ) Z -> X = Z ) )

Proof

Step	Hyp	Ref	Expression
1		frege103.z	|- Z e. V
2	1	elexi	|- Z e. _V
3		eqeq1	|- ( z = Z -> ( z = X <-> Z = X ) )
4		eqeq2	|- ( z = Z -> ( X = z <-> X = Z ) )
5	3 4	imbi12d	|- ( z = Z -> ( ( z = X -> X = z ) <-> ( Z = X -> X = Z ) ) )
6		frege55c	|- ( z = X -> X = z )
7	2 5 6	vtocl	|- ( Z = X -> X = Z )
8	1	frege103	|- ( ( Z = X -> X = Z ) -> ( X ( ( t+ ` R ) u. _I ) Z -> ( -. X ( t+ ` R ) Z -> X = Z ) ) )
9	7 8	ax-mp	|- ( X ( ( t+ ` R ) u. _I ) Z -> ( -. X ( t+ ` R ) Z -> X = Z ) )