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 V V B A B V =

Proof

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