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 ) ) )