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 | |- ( [ y / x ] A e. x <-> A e. y ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfv | |- F/ x A e. w |
|
| 2 | 1 | sbco2 | |- ( [ y / x ] [ x / w ] A e. w <-> [ y / w ] A e. w ) |
| 3 | nfv | |- F/ w A e. x |
|
| 4 | eleq2 | |- ( w = x -> ( A e. w <-> A e. x ) ) |
|
| 5 | 3 4 | sbie | |- ( [ x / w ] A e. w <-> A e. x ) |
| 6 | 5 | sbbii | |- ( [ y / x ] [ x / w ] A e. w <-> [ y / x ] A e. x ) |
| 7 | nfv | |- F/ w A e. y |
|
| 8 | eleq2 | |- ( w = y -> ( A e. w <-> A e. y ) ) |
|
| 9 | 7 8 | sbie | |- ( [ y / w ] A e. w <-> A e. y ) |
| 10 | 2 6 9 | 3bitr3i | |- ( [ y / x ] A e. x <-> A e. y ) |