**Description:** Deduce membership in an intersection of two classes. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

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

Hypotheses | elind.1 | $${\u22a2}{\phi}\to {X}\in {A}$$ | |

elind.2 | $${\u22a2}{\phi}\to {X}\in {B}$$ | ||

Assertion | elind | $${\u22a2}{\phi}\to {X}\in \left({A}\cap {B}\right)$$ |

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

1 | elind.1 | $${\u22a2}{\phi}\to {X}\in {A}$$ | |

2 | elind.2 | $${\u22a2}{\phi}\to {X}\in {B}$$ | |

3 | elin | $${\u22a2}{X}\in \left({A}\cap {B}\right)\leftrightarrow \left({X}\in {A}\wedge {X}\in {B}\right)$$ | |

4 | 1 2 3 | sylanbrc | $${\u22a2}{\phi}\to {X}\in \left({A}\cap {B}\right)$$ |