Metamath Proof Explorer


Theorem frege80

Description: Add additional condition to both clauses of frege79 . Proposition 80 of Frege1879 p. 63. (Contributed by RP, 1-Jul-2020) (Revised by RP, 5-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege80.x X U
frege80.y Y V
frege80.r R W
frege80.a A B
Assertion frege80 X A R hereditary A a X R a a A X A R hereditary A X t+ R Y Y A

Proof

Step Hyp Ref Expression
1 frege80.x X U
2 frege80.y Y V
3 frege80.r R W
4 frege80.a A B
5 1 2 3 4 frege79 R hereditary A a X R a a A R hereditary A X t+ R Y Y A
6 frege5 R hereditary A a X R a a A R hereditary A X t+ R Y Y A X A R hereditary A a X R a a A X A R hereditary A X t+ R Y Y A
7 5 6 ax-mp X A R hereditary A a X R a a A X A R hereditary A X t+ R Y Y A