Metamath Proof Explorer


Theorem disjOLD

Description: Obsolete version of disj as of 28-Jun-2024. (Contributed by NM, 17-Feb-2004) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion disjOLD A B = x A ¬ x B

Proof

Step Hyp Ref Expression
1 df-in A B = x | x A x B
2 1 eqeq1i A B = x | x A x B =
3 abeq1 x | x A x B = x x A x B x
4 imnan x A ¬ x B ¬ x A x B
5 noel ¬ x
6 5 nbn ¬ x A x B x A x B x
7 4 6 bitr2i x A x B x x A ¬ x B
8 7 albii x x A x B x x x A ¬ x B
9 2 3 8 3bitri A B = x x A ¬ x B
10 df-ral x A ¬ x B x x A ¬ x B
11 9 10 bitr4i A B = x A ¬ x B