Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Usage of the weaker cbvabw and cbvabv are preferred. (Contributed by Andrew Salmon, 11-Jul-2011) (Proof shortened by Wolf Lammen, 16-Nov-2019) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cbvab.1 | ⊢ Ⅎ 𝑦 𝜑 | |
cbvab.2 | ⊢ Ⅎ 𝑥 𝜓 | ||
cbvab.3 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | ||
Assertion | cbvab | ⊢ { 𝑥 ∣ 𝜑 } = { 𝑦 ∣ 𝜓 } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvab.1 | ⊢ Ⅎ 𝑦 𝜑 | |
2 | cbvab.2 | ⊢ Ⅎ 𝑥 𝜓 | |
3 | cbvab.3 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
4 | 1 | sbco2 | ⊢ ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) |
5 | 2 3 | sbie | ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) |
6 | 5 | sbbii | ⊢ ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜓 ) |
7 | 4 6 | bitr3i | ⊢ ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜓 ) |
8 | df-clab | ⊢ ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑧 / 𝑥 ] 𝜑 ) | |
9 | df-clab | ⊢ ( 𝑧 ∈ { 𝑦 ∣ 𝜓 } ↔ [ 𝑧 / 𝑦 ] 𝜓 ) | |
10 | 7 8 9 | 3bitr4i | ⊢ ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑧 ∈ { 𝑦 ∣ 𝜓 } ) |
11 | 10 | eqriv | ⊢ { 𝑥 ∣ 𝜑 } = { 𝑦 ∣ 𝜓 } |