Metamath Proof Explorer

Theorem frege105

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

Ref Expression
Hypothesis frege103.z ⊢ Z ∈ V
Assertion frege105 ⊢ ¬ X t+ ⁡ R Z → Z = X → X t+ ⁡ R ∪ I Z

Proof

Step Hyp Ref Expression
1 frege103.z ⊢ Z ∈ V
2 1 dffrege99 ⊢ ¬ X t+ ⁡ R Z → Z = X ↔ X t+ ⁡ R ∪ I Z
3 frege52aid ⊢ ¬ X t+ ⁡ R Z → Z = X ↔ X t+ ⁡ R ∪ I Z → ¬ X t+ ⁡ R Z → Z = X → X t+ ⁡ R ∪ I Z
4 2 3 ax-mp ⊢ ¬ X t+ ⁡ R Z → Z = X → X t+ ⁡ R ∪ I Z