Metamath Proof Explorer


Theorem reldisjOLD

Description: Obsolete version of reldisj as of 28-Jun-2024. (Contributed by NM, 15-Feb-2007) (Proof shortened by Andrew Salmon, 26-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion reldisjOLD ( 𝐴𝐶 → ( ( 𝐴𝐵 ) = ∅ ↔ 𝐴 ⊆ ( 𝐶𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 dfss2 ( 𝐴𝐶 ↔ ∀ 𝑥 ( 𝑥𝐴𝑥𝐶 ) )
2 pm5.44 ( ( 𝑥𝐴𝑥𝐶 ) → ( ( 𝑥𝐴 → ¬ 𝑥𝐵 ) ↔ ( 𝑥𝐴 → ( 𝑥𝐶 ∧ ¬ 𝑥𝐵 ) ) ) )
3 eldif ( 𝑥 ∈ ( 𝐶𝐵 ) ↔ ( 𝑥𝐶 ∧ ¬ 𝑥𝐵 ) )
4 3 imbi2i ( ( 𝑥𝐴𝑥 ∈ ( 𝐶𝐵 ) ) ↔ ( 𝑥𝐴 → ( 𝑥𝐶 ∧ ¬ 𝑥𝐵 ) ) )
5 2 4 bitr4di ( ( 𝑥𝐴𝑥𝐶 ) → ( ( 𝑥𝐴 → ¬ 𝑥𝐵 ) ↔ ( 𝑥𝐴𝑥 ∈ ( 𝐶𝐵 ) ) ) )
6 5 sps ( ∀ 𝑥 ( 𝑥𝐴𝑥𝐶 ) → ( ( 𝑥𝐴 → ¬ 𝑥𝐵 ) ↔ ( 𝑥𝐴𝑥 ∈ ( 𝐶𝐵 ) ) ) )
7 1 6 sylbi ( 𝐴𝐶 → ( ( 𝑥𝐴 → ¬ 𝑥𝐵 ) ↔ ( 𝑥𝐴𝑥 ∈ ( 𝐶𝐵 ) ) ) )
8 7 albidv ( 𝐴𝐶 → ( ∀ 𝑥 ( 𝑥𝐴 → ¬ 𝑥𝐵 ) ↔ ∀ 𝑥 ( 𝑥𝐴𝑥 ∈ ( 𝐶𝐵 ) ) ) )
9 disj1 ( ( 𝐴𝐵 ) = ∅ ↔ ∀ 𝑥 ( 𝑥𝐴 → ¬ 𝑥𝐵 ) )
10 dfss2 ( 𝐴 ⊆ ( 𝐶𝐵 ) ↔ ∀ 𝑥 ( 𝑥𝐴𝑥 ∈ ( 𝐶𝐵 ) ) )
11 8 9 10 3bitr4g ( 𝐴𝐶 → ( ( 𝐴𝐵 ) = ∅ ↔ 𝐴 ⊆ ( 𝐶𝐵 ) ) )