Metamath Proof Explorer

Theorem frege71

Description: Lemma for frege72 . Proposition 71 of Frege1879 p. 59. (Contributed by RP, 28-Mar-2020) (Revised by RP, 3-Jul-2020) (Proof modification is discouraged.)

		Ref	Expression
	Hypothesis	frege71.x	$⊢ X \in V$
	Assertion	frege71	$⊢ (\forall z (X R z \to z \in A) \to (X R Y \to Y \in A)) \to (R hereditary A \to (X \in A \to (X R Y \to Y \in A)))$

Proof

Step	Hyp	Ref	Expression
1		frege71.x	$⊢ X \in V$
2	1	frege70	$⊢ R hereditary A \to (X \in A \to \forall z (X R z \to z \in A))$
3		frege19	$⊢ (R hereditary A \to (X \in A \to \forall z (X R z \to z \in A))) \to ((\forall z (X R z \to z \in A) \to (X R Y \to Y \in A)) \to (R hereditary A \to (X \in A \to (X R Y \to Y \in A))))$
4	2 3	ax-mp	$⊢ (\forall z (X R z \to z \in A) \to (X R Y \to Y \in A)) \to (R hereditary A \to (X \in A \to (X R Y \to Y \in A)))$