Metamath Proof Explorer

Theorem frege89

Description: One direction of dffrege76 . Proposition 89 of Frege1879 p. 68. (Contributed by RP, 1-Jul-2020) (Revised by RP, 2-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege89.x ⊢ X ∈ U
frege89.y ⊢ Y ∈ V
frege89.r ⊢ R ∈ W
Assertion frege89 ⊢ ∀ f R hereditary f → ∀ w X R w → w ∈ f → Y ∈ f → X t+ ⁡ R Y

Proof

Step Hyp Ref Expression
1 frege89.x ⊢ X ∈ U
2 frege89.y ⊢ Y ∈ V
3 frege89.r ⊢ R ∈ W
4 1 2 3 dffrege76 ⊢ ∀ f R hereditary f → ∀ w X R w → w ∈ f → Y ∈ f ↔ X t+ ⁡ R Y
5 frege52aid ⊢ ∀ f R hereditary f → ∀ w X R w → w ∈ f → Y ∈ f ↔ X t+ ⁡ R Y → ∀ f R hereditary f → ∀ w X R w → w ∈ f → Y ∈ f → X t+ ⁡ R Y
6 4 5 ax-mp ⊢ ∀ f R hereditary f → ∀ w X R w → w ∈ f → Y ∈ f → X t+ ⁡ R Y