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 ( ( 𝜑𝑥𝐴 ) → ( 𝑥𝐵𝜓 ) )
Assertion rabbi2dva ( 𝜑 → ( 𝐴𝐵 ) = { 𝑥𝐴𝜓 } )

Proof

Step Hyp Ref Expression
1 rabbi2dva.1 ( ( 𝜑𝑥𝐴 ) → ( 𝑥𝐵𝜓 ) )
2 dfin5 ( 𝐴𝐵 ) = { 𝑥𝐴𝑥𝐵 }
3 1 rabbidva ( 𝜑 → { 𝑥𝐴𝑥𝐵 } = { 𝑥𝐴𝜓 } )
4 2 3 syl5eq ( 𝜑 → ( 𝐴𝐵 ) = { 𝑥𝐴𝜓 } )