Metamath Proof Explorer


Theorem chrelat3

Description: A consequence of relative atomicity. (Contributed by NM, 2-Jul-2004) (New usage is discouraged.)

Ref Expression
Assertion chrelat3 A C B C A B x HAtoms x A x B

Proof

Step Hyp Ref Expression
1 chrelat2 A C B C ¬ A B x HAtoms x A ¬ x B
2 dfrex2 x HAtoms x A ¬ x B ¬ x HAtoms ¬ x A ¬ x B
3 1 2 bitrdi A C B C ¬ A B ¬ x HAtoms ¬ x A ¬ x B
4 3 con4bid A C B C A B x HAtoms ¬ x A ¬ x B
5 iman x A x B ¬ x A ¬ x B
6 5 ralbii x HAtoms x A x B x HAtoms ¬ x A ¬ x B
7 4 6 bitr4di A C B C A B x HAtoms x A x B