Description: Obsolete version of clelsb2 as of 24-Nov-2024.) (Contributed by Jim Kingdon, 22-Nov-2018) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | clelsb2OLD | ⊢ ( [ 𝑦 / 𝑥 ] 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfv | ⊢ Ⅎ 𝑥 𝐴 ∈ 𝑤 | |
| 2 | 1 | sbco2 | ⊢ ( [ 𝑦 / 𝑥 ] [ 𝑥 / 𝑤 ] 𝐴 ∈ 𝑤 ↔ [ 𝑦 / 𝑤 ] 𝐴 ∈ 𝑤 ) |
| 3 | nfv | ⊢ Ⅎ 𝑤 𝐴 ∈ 𝑥 | |
| 4 | eleq2 | ⊢ ( 𝑤 = 𝑥 → ( 𝐴 ∈ 𝑤 ↔ 𝐴 ∈ 𝑥 ) ) | |
| 5 | 3 4 | sbie | ⊢ ( [ 𝑥 / 𝑤 ] 𝐴 ∈ 𝑤 ↔ 𝐴 ∈ 𝑥 ) |
| 6 | 5 | sbbii | ⊢ ( [ 𝑦 / 𝑥 ] [ 𝑥 / 𝑤 ] 𝐴 ∈ 𝑤 ↔ [ 𝑦 / 𝑥 ] 𝐴 ∈ 𝑥 ) |
| 7 | nfv | ⊢ Ⅎ 𝑤 𝐴 ∈ 𝑦 | |
| 8 | eleq2 | ⊢ ( 𝑤 = 𝑦 → ( 𝐴 ∈ 𝑤 ↔ 𝐴 ∈ 𝑦 ) ) | |
| 9 | 7 8 | sbie | ⊢ ( [ 𝑦 / 𝑤 ] 𝐴 ∈ 𝑤 ↔ 𝐴 ∈ 𝑦 ) |
| 10 | 2 6 9 | 3bitr3i | ⊢ ( [ 𝑦 / 𝑥 ] 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦 ) |