Description: Obsolete version of cbvralsvw as of 8-Mar-2025. (Contributed by NM, 20-Nov-2005) Avoid ax-13 . (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | cbvralsvwOLD | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 [ 𝑦 / 𝑥 ] 𝜑 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv | ⊢ Ⅎ 𝑧 𝜑 | |
2 | nfs1v | ⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑 | |
3 | sbequ12 | ⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) ) | |
4 | 1 2 3 | cbvralw | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑧 ∈ 𝐴 [ 𝑧 / 𝑥 ] 𝜑 ) |
5 | nfv | ⊢ Ⅎ 𝑦 [ 𝑧 / 𝑥 ] 𝜑 | |
6 | nfv | ⊢ Ⅎ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 | |
7 | sbequ | ⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) ) | |
8 | 5 6 7 | cbvralw | ⊢ ( ∀ 𝑧 ∈ 𝐴 [ 𝑧 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 [ 𝑦 / 𝑥 ] 𝜑 ) |
9 | 4 8 | bitri | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 [ 𝑦 / 𝑥 ] 𝜑 ) |