Metamath Proof Explorer


Theorem reldisjOLD

Description: Obsolete version of reldisj as of 28-Jun-2024. (Contributed by NM, 15-Feb-2007) (Proof shortened by Andrew Salmon, 26-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion reldisjOLD
|- ( A C_ C -> ( ( A i^i B ) = (/) <-> A C_ ( C \ B ) ) )

Proof

Step Hyp Ref Expression
1 dfss2
 |-  ( A C_ C <-> A. x ( x e. A -> x e. C ) )
2 pm5.44
 |-  ( ( x e. A -> x e. C ) -> ( ( x e. A -> -. x e. B ) <-> ( x e. A -> ( x e. C /\ -. x e. B ) ) ) )
3 eldif
 |-  ( x e. ( C \ B ) <-> ( x e. C /\ -. x e. B ) )
4 3 imbi2i
 |-  ( ( x e. A -> x e. ( C \ B ) ) <-> ( x e. A -> ( x e. C /\ -. x e. B ) ) )
5 2 4 bitr4di
 |-  ( ( x e. A -> x e. C ) -> ( ( x e. A -> -. x e. B ) <-> ( x e. A -> x e. ( C \ B ) ) ) )
6 5 sps
 |-  ( A. x ( x e. A -> x e. C ) -> ( ( x e. A -> -. x e. B ) <-> ( x e. A -> x e. ( C \ B ) ) ) )
7 1 6 sylbi
 |-  ( A C_ C -> ( ( x e. A -> -. x e. B ) <-> ( x e. A -> x e. ( C \ B ) ) ) )
8 7 albidv
 |-  ( A C_ C -> ( A. x ( x e. A -> -. x e. B ) <-> A. x ( x e. A -> x e. ( C \ B ) ) ) )
9 disj1
 |-  ( ( A i^i B ) = (/) <-> A. x ( x e. A -> -. x e. B ) )
10 dfss2
 |-  ( A C_ ( C \ B ) <-> A. x ( x e. A -> x e. ( C \ B ) ) )
11 8 9 10 3bitr4g
 |-  ( A C_ C -> ( ( A i^i B ) = (/) <-> A C_ ( C \ B ) ) )