**Description:** Deduction from a wff to a restricted class abstraction. (Contributed by NM, 14-Jan-2014)

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

Hypothesis | rabbi2dva.1 | $${\u22a2}\left({\phi}\wedge {x}\in {A}\right)\to \left({x}\in {B}\leftrightarrow {\psi}\right)$$ | |

Assertion | rabbi2dva | $${\u22a2}{\phi}\to {A}\cap {B}=\left\{{x}\in {A}|{\psi}\right\}$$ |

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

1 | rabbi2dva.1 | $${\u22a2}\left({\phi}\wedge {x}\in {A}\right)\to \left({x}\in {B}\leftrightarrow {\psi}\right)$$ | |

2 | dfin5 | $${\u22a2}{A}\cap {B}=\left\{{x}\in {A}|{x}\in {B}\right\}$$ | |

3 | 1 | rabbidva | $${\u22a2}{\phi}\to \left\{{x}\in {A}|{x}\in {B}\right\}=\left\{{x}\in {A}|{\psi}\right\}$$ |

4 | 2 3 | syl5eq | $${\u22a2}{\phi}\to {A}\cap {B}=\left\{{x}\in {A}|{\psi}\right\}$$ |