Metamath Proof Explorer


Theorem bj-rabeqd

Description: Deduction form of rabeq . Note that contrary to rabeq it has no disjoint variable condition. (Contributed by BJ, 27-Apr-2019)

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

Proof

Step Hyp Ref Expression
1 bj-rabeqd.nf 𝑥 𝜑
2 bj-rabeqd.1 ( 𝜑𝐴 = 𝐵 )
3 eleq2 ( 𝐴 = 𝐵 → ( 𝑥𝐴𝑥𝐵 ) )
4 3 anbi1d ( 𝐴 = 𝐵 → ( ( 𝑥𝐴𝜓 ) ↔ ( 𝑥𝐵𝜓 ) ) )
5 2 4 syl ( 𝜑 → ( ( 𝑥𝐴𝜓 ) ↔ ( 𝑥𝐵𝜓 ) ) )
6 1 5 bj-rabbida2 ( 𝜑 → { 𝑥𝐴𝜓 } = { 𝑥𝐵𝜓 } )