Metamath Proof Explorer


Theorem bj-disj2r

Description: Relative version of ssdifin0 , allowing a biconditional, and of disj2 . (Contributed by BJ, 11-Nov-2021) This proof does not rely, even indirectly, on ssdifin0 nor disj2 . (Proof modification is discouraged.)

Ref Expression
Assertion bj-disj2r
|- ( ( A i^i V ) C_ ( V \ B ) <-> ( ( A i^i B ) i^i V ) = (/) )

Proof

Step Hyp Ref Expression
1 df-ss
 |-  ( ( A i^i V ) C_ ( V \ B ) <-> ( ( A i^i V ) i^i ( V \ B ) ) = ( A i^i V ) )
2 indif2
 |-  ( ( A i^i V ) i^i ( V \ B ) ) = ( ( ( A i^i V ) i^i V ) \ B )
3 inss1
 |-  ( ( A i^i V ) i^i V ) C_ ( A i^i V )
4 ssid
 |-  ( A i^i V ) C_ ( A i^i V )
5 inss2
 |-  ( A i^i V ) C_ V
6 4 5 ssini
 |-  ( A i^i V ) C_ ( ( A i^i V ) i^i V )
7 3 6 eqssi
 |-  ( ( A i^i V ) i^i V ) = ( A i^i V )
8 7 difeq1i
 |-  ( ( ( A i^i V ) i^i V ) \ B ) = ( ( A i^i V ) \ B )
9 2 8 eqtri
 |-  ( ( A i^i V ) i^i ( V \ B ) ) = ( ( A i^i V ) \ B )
10 9 eqeq1i
 |-  ( ( ( A i^i V ) i^i ( V \ B ) ) = ( A i^i V ) <-> ( ( A i^i V ) \ B ) = ( A i^i V ) )
11 eqcom
 |-  ( ( ( A i^i V ) \ B ) = ( A i^i V ) <-> ( A i^i V ) = ( ( A i^i V ) \ B ) )
12 1 10 11 3bitri
 |-  ( ( A i^i V ) C_ ( V \ B ) <-> ( A i^i V ) = ( ( A i^i V ) \ B ) )
13 disj3
 |-  ( ( ( A i^i V ) i^i B ) = (/) <-> ( A i^i V ) = ( ( A i^i V ) \ B ) )
14 in32
 |-  ( ( A i^i V ) i^i B ) = ( ( A i^i B ) i^i V )
15 14 eqeq1i
 |-  ( ( ( A i^i V ) i^i B ) = (/) <-> ( ( A i^i B ) i^i V ) = (/) )
16 12 13 15 3bitr2i
 |-  ( ( A i^i V ) C_ ( V \ B ) <-> ( ( A i^i B ) i^i V ) = (/) )