Metamath Proof Explorer


Theorem frege83d

Description: If the image of the union of U and V is a subset of the union of U and V , A is an element of U and B follows A in the transitive closure of R , then B is an element of the union of U and V . Similar to Proposition 83 of Frege1879 p. 65. Compare with frege83 . (Contributed by RP, 15-Jul-2020)

Ref Expression
Hypotheses frege83d.r φ R V
frege83d.a φ A U
frege83d.b φ B V
frege83d.ab φ A t+ R B
frege83d.he φ R U V U V
Assertion frege83d φ B U V

Proof

Step Hyp Ref Expression
1 frege83d.r φ R V
2 frege83d.a φ A U
3 frege83d.b φ B V
4 frege83d.ab φ A t+ R B
5 frege83d.he φ R U V U V
6 ssun1 U U V
7 6 2 sseldi φ A U V
8 1 7 3 4 5 frege81d φ B U V