Metamath Proof Explorer


Theorem inpr0

Description: Rewrite an empty intersection with a pair. (Contributed by Thierry Arnoux, 20-Nov-2023)

Ref Expression
Assertion inpr0 A B C = ¬ B A ¬ C A

Proof

Step Hyp Ref Expression
1 r19.26 x A x B x C x A x B x A x C
2 nelpr x V ¬ x B C x B x C
3 2 elv ¬ x B C x B x C
4 3 imbi2i x A ¬ x B C x A x B x C
5 4 albii x x A ¬ x B C x x A x B x C
6 disj1 A B C = x x A ¬ x B C
7 df-ral x A x B x C x x A x B x C
8 5 6 7 3bitr4i A B C = x A x B x C
9 nelb ¬ B A x A x B
10 nelb ¬ C A x A x C
11 9 10 anbi12i ¬ B A ¬ C A x A x B x A x C
12 1 8 11 3bitr4i A B C = ¬ B A ¬ C A