Description: Set substitution into the first argument of a subset relation. (Contributed by Rodolfo Medina, 7-Jul-2010) (Proof shortened by Mario Carneiro, 14-Nov-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sbss | |- ( [ y / x ] x C_ A <-> y C_ A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sseq1 | |- ( x = z -> ( x C_ A <-> z C_ A ) ) |
|
| 2 | sseq1 | |- ( z = y -> ( z C_ A <-> y C_ A ) ) |
|
| 3 | 1 2 | sbievw2 | |- ( [ y / x ] x C_ A <-> y C_ A ) |