Description: Contraposition law for relative subclasses. Relative and generalized version of ssconb . Shortens ssconb , conss2 . (Contributed by BJ, 11-Nov-2021) This proof does not rely, even indirectly, on ssconb nor conss2 . (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-sscon | |- ( ( A i^i V ) C_ ( V \ B ) <-> ( B i^i V ) C_ ( V \ A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | incom | |- ( A i^i B ) = ( B i^i A ) |
|
| 2 | 1 | ineq1i | |- ( ( A i^i B ) i^i V ) = ( ( B i^i A ) i^i V ) |
| 3 | 2 | eqeq1i | |- ( ( ( A i^i B ) i^i V ) = (/) <-> ( ( B i^i A ) i^i V ) = (/) ) |
| 4 | bj-disj2r | |- ( ( A i^i V ) C_ ( V \ B ) <-> ( ( A i^i B ) i^i V ) = (/) ) |
|
| 5 | bj-disj2r | |- ( ( B i^i V ) C_ ( V \ A ) <-> ( ( B i^i A ) i^i V ) = (/) ) |
|
| 6 | 3 4 5 | 3bitr4i | |- ( ( A i^i V ) C_ ( V \ B ) <-> ( B i^i V ) C_ ( V \ A ) ) |