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		dfss2	|- ( ( 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 ) = (/) )