Metamath Proof Explorer


Theorem frege127

Description: Communte antecedents of frege126 . Proposition 127 of Frege1879 p. 82. (Contributed by RP, 9-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege123.x X U
frege123.y Y V
frege124.m M W
frege124.r R S
Assertion frege127 Fun R -1 -1 Y t+ R M Y R X ¬ X t+ R M M t+ R I X

Proof

Step Hyp Ref Expression
1 frege123.x X U
2 frege123.y Y V
3 frege124.m M W
4 frege124.r R S
5 1 2 3 4 frege126 Fun R -1 -1 Y R X Y t+ R M ¬ X t+ R M M t+ R I X
6 frege12 Fun R -1 -1 Y R X Y t+ R M ¬ X t+ R M M t+ R I X Fun R -1 -1 Y t+ R M Y R X ¬ X t+ R M M t+ R I X
7 5 6 ax-mp Fun R -1 -1 Y t+ R M Y R X ¬ X t+ R M M t+ R I X