Metamath Proof Explorer


Theorem rabbi2dva

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

Ref Expression
Hypothesis rabbi2dva.1
|- ( ( ph /\ x e. A ) -> ( x e. B <-> ps ) )
Assertion rabbi2dva
|- ( ph -> ( A i^i B ) = { x e. A | ps } )

Proof

Step Hyp Ref Expression
1 rabbi2dva.1
 |-  ( ( ph /\ x e. A ) -> ( x e. B <-> ps ) )
2 dfin5
 |-  ( A i^i B ) = { x e. A | x e. B }
3 1 rabbidva
 |-  ( ph -> { x e. A | x e. B } = { x e. A | ps } )
4 2 3 syl5eq
 |-  ( ph -> ( A i^i B ) = { x e. A | ps } )