Description: Substitution for the second argument of the membership predicate in an atomic formula (class version of elsb2 ). (Contributed by Jim Kingdon, 22-Nov-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | clelsb2 | ⊢ ( [ 𝑦 / 𝑥 ] 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦 ) |
| 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 | ⊢ ( [ 𝑦 / 𝑥 ] 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦 ) |