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 } ) |
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 } ) |