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 ( ( 𝐴C𝐵C ) → ( 𝐴𝐵 ↔ ∀ 𝑥 ∈ HAtoms ( 𝑥𝐴𝑥𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 chrelat2 ( ( 𝐴C𝐵C ) → ( ¬ 𝐴𝐵 ↔ ∃ 𝑥 ∈ HAtoms ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) ) )
2 dfrex2 ( ∃ 𝑥 ∈ HAtoms ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) ↔ ¬ ∀ 𝑥 ∈ HAtoms ¬ ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) )
3 1 2 bitrdi ( ( 𝐴C𝐵C ) → ( ¬ 𝐴𝐵 ↔ ¬ ∀ 𝑥 ∈ HAtoms ¬ ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) ) )
4 3 con4bid ( ( 𝐴C𝐵C ) → ( 𝐴𝐵 ↔ ∀ 𝑥 ∈ HAtoms ¬ ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) ) )
5 iman ( ( 𝑥𝐴𝑥𝐵 ) ↔ ¬ ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) )
6 5 ralbii ( ∀ 𝑥 ∈ HAtoms ( 𝑥𝐴𝑥𝐵 ) ↔ ∀ 𝑥 ∈ HAtoms ¬ ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) )
7 4 6 bitr4di ( ( 𝐴C𝐵C ) → ( 𝐴𝐵 ↔ ∀ 𝑥 ∈ HAtoms ( 𝑥𝐴𝑥𝐵 ) ) )