**Description:** Elementhood in the first set of an intersection - deduction version.
(Contributed by Thierry Arnoux, 3-May-2020)

Ref | Expression | ||
---|---|---|---|

Hypothesis | elin1d.1 | $${\u22a2}{\phi}\to {X}\in \left({A}\cap {B}\right)$$ | |

Assertion | elin2d | $${\u22a2}{\phi}\to {X}\in {B}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | elin1d.1 | $${\u22a2}{\phi}\to {X}\in \left({A}\cap {B}\right)$$ | |

2 | elinel2 | $${\u22a2}{X}\in \left({A}\cap {B}\right)\to {X}\in {B}$$ | |

3 | 1 2 | syl | $${\u22a2}{\phi}\to {X}\in {B}$$ |