Description: Equality theorem for restricted class abstractions. Inference form of rabeqf . (Contributed by Glauco Siliprandi, 26-Jun-2021) Avoid ax-10 and ax-11 . (Revised by Gino Giotto, 20-Aug-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | rabeqi.1 | ⊢ 𝐴 = 𝐵 | |
| Assertion | rabeqi | ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∈ 𝐵 ∣ 𝜑 } |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rabeqi.1 | ⊢ 𝐴 = 𝐵 | |
| 2 | 1 | nfth | ⊢ Ⅎ 𝑥 𝐴 = 𝐵 |
| 3 | eleq2 | ⊢ ( 𝐴 = 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) | |
| 4 | 3 | anbi1d | ⊢ ( 𝐴 = 𝐵 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) ) |
| 5 | 2 4 | abbid | ⊢ ( 𝐴 = 𝐵 → { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } ) |
| 6 | df-rab | ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } | |
| 7 | df-rab | ⊢ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } | |
| 8 | 5 6 7 | 3eqtr4g | ⊢ ( 𝐴 = 𝐵 → { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∈ 𝐵 ∣ 𝜑 } ) |
| 9 | 1 8 | ax-mp | ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∈ 𝐵 ∣ 𝜑 } |