Metamath Proof Explorer


Theorem bj-rabbida2

Description: Version of rabbidva2 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019)

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

Proof

Step Hyp Ref Expression
1 bj-rabbida2.nf 𝑥 𝜑
2 bj-rabbida2.1 ( 𝜑 → ( ( 𝑥𝐴𝜓 ) ↔ ( 𝑥𝐵𝜒 ) ) )
3 1 2 abbid ( 𝜑 → { 𝑥 ∣ ( 𝑥𝐴𝜓 ) } = { 𝑥 ∣ ( 𝑥𝐵𝜒 ) } )
4 df-rab { 𝑥𝐴𝜓 } = { 𝑥 ∣ ( 𝑥𝐴𝜓 ) }
5 df-rab { 𝑥𝐵𝜒 } = { 𝑥 ∣ ( 𝑥𝐵𝜒 ) }
6 3 4 5 3eqtr4g ( 𝜑 → { 𝑥𝐴𝜓 } = { 𝑥𝐵𝜒 } )