Metamath Proof Explorer

Theorem frege103

Description: Proposition 103 of Frege1879 p. 73. (Contributed by RP, 7-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypothesis frege103.z 
|- Z e. V
Assertion frege103 
|- ( ( Z = X -> X = Z ) -> ( 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 frege100 
 |-  ( X ( ( t+ ` R ) u. _I ) Z -> ( -. X ( t+ ` R ) Z -> Z = X ) )
3 frege19 
 |-  ( ( X ( ( t+ ` R ) u. _I ) Z -> ( -. X ( t+ ` R ) Z -> Z = X ) ) -> ( ( Z = X -> X = Z ) -> ( X ( ( t+ ` R ) u. _I ) Z -> ( -. X ( t+ ` R ) Z -> X = Z ) ) ) )
4 2 3 ax-mp 
 |-  ( ( Z = X -> X = Z ) -> ( X ( ( t+ ` R ) u. _I ) Z -> ( -. X ( t+ ` R ) Z -> X = Z ) ) )