Metamath Proof Explorer


Theorem rabeqbidva

Description: Equality of restricted class abstractions. (Contributed by Mario Carneiro, 26-Jan-2017)

Ref Expression
Hypotheses rabeqbidva.1 φA=B
rabeqbidva.2 φxAψχ
Assertion rabeqbidva φxA|ψ=xB|χ

Proof

Step Hyp Ref Expression
1 rabeqbidva.1 φA=B
2 rabeqbidva.2 φxAψχ
3 2 rabbidva φxA|ψ=xA|χ
4 1 rabeqdv φxA|χ=xB|χ
5 3 4 eqtrd φxA|ψ=xB|χ