Metamath Proof Explorer


Theorem rabeq12f

Description: Equality deduction for restricted class abstraction. (Contributed by Giovanni Mascellani, 10-Apr-2018)

Ref Expression
Hypotheses rabeq12f.1
|- F/_ x A
rabeq12f.2
|- F/_ x B
Assertion rabeq12f
|- ( ( A = B /\ A. x e. A ( ph <-> ps ) ) -> { x e. A | ph } = { x e. B | ps } )

Proof

Step Hyp Ref Expression
1 rabeq12f.1
 |-  F/_ x A
2 rabeq12f.2
 |-  F/_ x B
3 rabbi
 |-  ( A. x e. A ( ph <-> ps ) <-> { x e. A | ph } = { x e. A | ps } )
4 3 biimpi
 |-  ( A. x e. A ( ph <-> ps ) -> { x e. A | ph } = { x e. A | ps } )
5 1 2 rabeqf
 |-  ( A = B -> { x e. A | ps } = { x e. B | ps } )
6 4 5 sylan9eqr
 |-  ( ( A = B /\ A. x e. A ( ph <-> ps ) ) -> { x e. A | ph } = { x e. B | ps } )