Description: Change bound variable by using a substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvrexsvw when possible. (Contributed by NM, 2-Mar-2008) (Revised by Andrew Salmon, 11-Jul-2011) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cbvrexsv | ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 [ 𝑦 / 𝑥 ] 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfv | ⊢ Ⅎ 𝑧 𝜑 | |
| 2 | nfs1v | ⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑 | |
| 3 | sbequ12 | ⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) ) | |
| 4 | 1 2 3 | cbvrex | ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑧 ∈ 𝐴 [ 𝑧 / 𝑥 ] 𝜑 ) |
| 5 | nfv | ⊢ Ⅎ 𝑦 𝜑 | |
| 6 | 5 | nfsb | ⊢ Ⅎ 𝑦 [ 𝑧 / 𝑥 ] 𝜑 |
| 7 | nfv | ⊢ Ⅎ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 | |
| 8 | sbequ | ⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) ) | |
| 9 | 6 7 8 | cbvrex | ⊢ ( ∃ 𝑧 ∈ 𝐴 [ 𝑧 / 𝑥 ] 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 [ 𝑦 / 𝑥 ] 𝜑 ) |
| 10 | 4 9 | bitri | ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 [ 𝑦 / 𝑥 ] 𝜑 ) |