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 φ x A x B ψ
Assertion rabbi2dva φ A B = x A | ψ

Proof

Step Hyp Ref Expression
1 rabbi2dva.1 φ x A x B ψ
2 dfin5 A B = x A | x B
3 1 rabbidva φ x A | x B = x A | ψ
4 2 3 syl5eq φ A B = x A | ψ