Metamath Proof Explorer


Theorem eqrrabd

Description: Deduce equality with a restricted abstraction. (Contributed by Thierry Arnoux, 11-Apr-2024)

Ref Expression
Hypotheses eqrrabd.1 ( 𝜑𝐵𝐴 )
eqrrabd.2 ( ( 𝜑𝑥𝐴 ) → ( 𝑥𝐵𝜓 ) )
Assertion eqrrabd ( 𝜑𝐵 = { 𝑥𝐴𝜓 } )

Proof

Step Hyp Ref Expression
1 eqrrabd.1 ( 𝜑𝐵𝐴 )
2 eqrrabd.2 ( ( 𝜑𝑥𝐴 ) → ( 𝑥𝐵𝜓 ) )
3 nfv 𝑥 𝜑
4 nfcv 𝑥 𝐵
5 nfrab1 𝑥 { 𝑥𝐴𝜓 }
6 1 sseld ( 𝜑 → ( 𝑥𝐵𝑥𝐴 ) )
7 6 pm4.71rd ( 𝜑 → ( 𝑥𝐵 ↔ ( 𝑥𝐴𝑥𝐵 ) ) )
8 2 pm5.32da ( 𝜑 → ( ( 𝑥𝐴𝑥𝐵 ) ↔ ( 𝑥𝐴𝜓 ) ) )
9 7 8 bitrd ( 𝜑 → ( 𝑥𝐵 ↔ ( 𝑥𝐴𝜓 ) ) )
10 rabid ( 𝑥 ∈ { 𝑥𝐴𝜓 } ↔ ( 𝑥𝐴𝜓 ) )
11 9 10 bitr4di ( 𝜑 → ( 𝑥𝐵𝑥 ∈ { 𝑥𝐴𝜓 } ) )
12 3 4 5 11 eqrd ( 𝜑𝐵 = { 𝑥𝐴𝜓 } )