This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐵 = { 𝑥 ∈ 𝐴 ∣ 𝜓 } )