Description: Obsolete version of cbvabw as of 23-May-2024. (Contributed by Andrew Salmon, 11-Jul-2011) (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cbvabwOLD.1 | ⊢ Ⅎ 𝑦 𝜑 | |
cbvabwOLD.2 | ⊢ Ⅎ 𝑥 𝜓 | ||
cbvabwOLD.3 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | ||
Assertion | cbvabwOLD | ⊢ { 𝑥 ∣ 𝜑 } = { 𝑦 ∣ 𝜓 } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvabwOLD.1 | ⊢ Ⅎ 𝑦 𝜑 | |
2 | cbvabwOLD.2 | ⊢ Ⅎ 𝑥 𝜓 | |
3 | cbvabwOLD.3 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
4 | 1 | sbco2v | ⊢ ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) |
5 | 2 3 | sbiev | ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) |
6 | 5 | sbbii | ⊢ ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜓 ) |
7 | 4 6 | bitr3i | ⊢ ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜓 ) |
8 | df-clab | ⊢ ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑧 / 𝑥 ] 𝜑 ) | |
9 | df-clab | ⊢ ( 𝑧 ∈ { 𝑦 ∣ 𝜓 } ↔ [ 𝑧 / 𝑦 ] 𝜓 ) | |
10 | 7 8 9 | 3bitr4i | ⊢ ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑧 ∈ { 𝑦 ∣ 𝜓 } ) |
11 | 10 | eqriv | ⊢ { 𝑥 ∣ 𝜑 } = { 𝑦 ∣ 𝜓 } |