Metamath Proof Explorer


Theorem raleqbid

Description: Equality deduction for restricted universal quantifier. (Contributed by Thierry Arnoux, 8-Mar-2017)

Ref Expression
Hypotheses raleqbid.0
|- F/ x ph
raleqbid.1
|- F/_ x A
raleqbid.2
|- F/_ x B
raleqbid.3
|- ( ph -> A = B )
raleqbid.4
|- ( ph -> ( ps <-> ch ) )
Assertion raleqbid
|- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )

Proof

Step Hyp Ref Expression
1 raleqbid.0
 |-  F/ x ph
2 raleqbid.1
 |-  F/_ x A
3 raleqbid.2
 |-  F/_ x B
4 raleqbid.3
 |-  ( ph -> A = B )
5 raleqbid.4
 |-  ( ph -> ( ps <-> ch ) )
6 2 3 raleqf
 |-  ( A = B -> ( A. x e. A ps <-> A. x e. B ps ) )
7 4 6 syl
 |-  ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )
8 1 5 ralbid
 |-  ( ph -> ( A. x e. B ps <-> A. x e. B ch ) )
9 7 8 bitrd
 |-  ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )