Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. (Contributed by NM, 26-May-1999) Require x , y be disjoint to avoid ax-11 and ax-13 . (Revised by Steven Nguyen, 4-Dec-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | cbvrabv.1 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
| Assertion | cbvrabv | ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 ∈ 𝐴 ∣ 𝜓 } |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvrabv.1 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
| 2 | eleq1w | ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) ) | |
| 3 | 2 1 | anbi12d | ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ) |
| 4 | 3 | cbvabv | ⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) } |
| 5 | df-rab | ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } | |
| 6 | df-rab | ⊢ { 𝑦 ∈ 𝐴 ∣ 𝜓 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) } | |
| 7 | 4 5 6 | 3eqtr4i | ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 ∈ 𝐴 ∣ 𝜓 } |