Metamath Proof Explorer


Theorem bj-rabeqbida

Description: Version of rabeqbidva with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019)

Ref Expression
Hypotheses bj-rabeqbida.nf 𝑥 𝜑
bj-rabeqbida.1 ( 𝜑𝐴 = 𝐵 )
bj-rabeqbida.2 ( ( 𝜑𝑥𝐴 ) → ( 𝜓𝜒 ) )
Assertion bj-rabeqbida ( 𝜑 → { 𝑥𝐴𝜓 } = { 𝑥𝐵𝜒 } )

Proof

Step Hyp Ref Expression
1 bj-rabeqbida.nf 𝑥 𝜑
2 bj-rabeqbida.1 ( 𝜑𝐴 = 𝐵 )
3 bj-rabeqbida.2 ( ( 𝜑𝑥𝐴 ) → ( 𝜓𝜒 ) )
4 1 3 rabbida ( 𝜑 → { 𝑥𝐴𝜓 } = { 𝑥𝐴𝜒 } )
5 1 2 bj-rabeqd ( 𝜑 → { 𝑥𝐴𝜒 } = { 𝑥𝐵𝜒 } )
6 4 5 eqtrd ( 𝜑 → { 𝑥𝐴𝜓 } = { 𝑥𝐵𝜒 } )