Metamath Proof Explorer

Theorem frege91

Description: Every result of an application of a procedure R to an object X follows that X in the R -sequence. Proposition 91 of Frege1879 p. 68. (Contributed by RP, 2-Jul-2020) (Revised by RP, 5-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege91.x ⊢ X ∈ U
frege91.y ⊢ Y ∈ V
frege91.r ⊢ R ∈ W
Assertion frege91 ⊢ X R Y → X t+ ⁡ R Y

Proof

Step Hyp Ref Expression
1 frege91.x ⊢ X ∈ U
2 frege91.y ⊢ Y ∈ V
3 frege91.r ⊢ R ∈ W
4 2 frege63c ⊢ [˙Y / a]˙ X R a → R hereditary f → ∀ a X R a → a ∈ f → [˙Y / a]˙ a ∈ f
5 sbcbr2g ⊢ Y ∈ V → [˙Y / a]˙ X R a ↔ X R ⦋ Y / a⦌ a
6 csbvarg ⊢ Y ∈ V → ⦋ Y / a⦌ a = Y
7 6 breq2d ⊢ Y ∈ V → X R ⦋ Y / a⦌ a ↔ X R Y
8 5 7 bitrd ⊢ Y ∈ V → [˙Y / a]˙ X R a ↔ X R Y
9 2 8 ax-mp ⊢ [˙Y / a]˙ X R a ↔ X R Y
10 sbcel1v ⊢ [˙Y / a]˙ a ∈ f ↔ Y ∈ f
11 10 imbi2i ⊢ ∀ a X R a → a ∈ f → [˙Y / a]˙ a ∈ f ↔ ∀ a X R a → a ∈ f → Y ∈ f
12 11 imbi2i ⊢ R hereditary f → ∀ a X R a → a ∈ f → [˙Y / a]˙ a ∈ f ↔ R hereditary f → ∀ a X R a → a ∈ f → Y ∈ f
13 4 9 12 3imtr3i ⊢ X R Y → R hereditary f → ∀ a X R a → a ∈ f → Y ∈ f
14 13 alrimiv ⊢ X R Y → ∀ f R hereditary f → ∀ a X R a → a ∈ f → Y ∈ f
15 1 2 3 frege90 ⊢ X R Y → ∀ f R hereditary f → ∀ a X R a → a ∈ f → Y ∈ f → X R Y → X t+ ⁡ R Y
16 14 15 ax-mp ⊢ X R Y → X t+ ⁡ R Y