Metamath Proof Explorer

Theorem frege101

Description: Lemma for frege102 . Proposition 101 of Frege1879 p. 72. (Contributed by RP, 7-Jul-2020) (Proof modification is discouraged.)

		Ref	Expression
	Hypothesis	frege99.z	$⊢ Z \in U$
	Assertion	frege101	$⊢ (Z = X \to (Z R V \to X t+ (R) V)) \to ((X t+ (R) Z \to (Z R V \to X t+ (R) V)) \to (X (t+ (R) \cup I) Z \to (Z R V \to X t+ (R) V)))$

Step	Hyp	Ref	Expression
1		frege99.z	$⊢ Z \in U$
2	1	frege100	$⊢ X (t+ (R) \cup I) Z \to (\neg X t+ (R) Z \to Z = X)$
3		frege48	$⊢ (X (t+ (R) \cup I) Z \to (\neg X t+ (R) Z \to Z = X)) \to ((Z = X \to (Z R V \to X t+ (R) V)) \to ((X t+ (R) Z \to (Z R V \to X t+ (R) V)) \to (X (t+ (R) \cup I) Z \to (Z R V \to X t+ (R) V))))$
4	2 3	ax-mp	$⊢ (Z = X \to (Z R V \to X t+ (R) V)) \to ((X t+ (R) Z \to (Z R V \to X t+ (R) V)) \to (X (t+ (R) \cup I) Z \to (Z R V \to X t+ (R) V)))$