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 e. CH /\ B e. CH ) -> ( A C_ B <-> A. x e. HAtoms ( x C_ A -> x C_ B ) ) )

Proof

Step Hyp Ref Expression
1 chrelat2
 |-  ( ( A e. CH /\ B e. CH ) -> ( -. A C_ B <-> E. x e. HAtoms ( x C_ A /\ -. x C_ B ) ) )
2 dfrex2
 |-  ( E. x e. HAtoms ( x C_ A /\ -. x C_ B ) <-> -. A. x e. HAtoms -. ( x C_ A /\ -. x C_ B ) )
3 1 2 bitrdi
 |-  ( ( A e. CH /\ B e. CH ) -> ( -. A C_ B <-> -. A. x e. HAtoms -. ( x C_ A /\ -. x C_ B ) ) )
4 3 con4bid
 |-  ( ( A e. CH /\ B e. CH ) -> ( A C_ B <-> A. x e. HAtoms -. ( x C_ A /\ -. x C_ B ) ) )
5 iman
 |-  ( ( x C_ A -> x C_ B ) <-> -. ( x C_ A /\ -. x C_ B ) )
6 5 ralbii
 |-  ( A. x e. HAtoms ( x C_ A -> x C_ B ) <-> A. x e. HAtoms -. ( x C_ A /\ -. x C_ B ) )
7 4 6 bitr4di
 |-  ( ( A e. CH /\ B e. CH ) -> ( A C_ B <-> A. x e. HAtoms ( x C_ A -> x C_ B ) ) )