Description: Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | disjss1f.1 | ⊢ Ⅎ 𝑥 𝐴 | |
disjss1f.2 | ⊢ Ⅎ 𝑥 𝐵 | ||
Assertion | disjeq1f | ⊢ ( 𝐴 = 𝐵 → ( Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | disjss1f.1 | ⊢ Ⅎ 𝑥 𝐴 | |
2 | disjss1f.2 | ⊢ Ⅎ 𝑥 𝐵 | |
3 | eqimss2 | ⊢ ( 𝐴 = 𝐵 → 𝐵 ⊆ 𝐴 ) | |
4 | 2 1 | disjss1f | ⊢ ( 𝐵 ⊆ 𝐴 → ( Disj 𝑥 ∈ 𝐴 𝐶 → Disj 𝑥 ∈ 𝐵 𝐶 ) ) |
5 | 3 4 | syl | ⊢ ( 𝐴 = 𝐵 → ( Disj 𝑥 ∈ 𝐴 𝐶 → Disj 𝑥 ∈ 𝐵 𝐶 ) ) |
6 | eqimss | ⊢ ( 𝐴 = 𝐵 → 𝐴 ⊆ 𝐵 ) | |
7 | 1 2 | disjss1f | ⊢ ( 𝐴 ⊆ 𝐵 → ( Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶 ) ) |
8 | 6 7 | syl | ⊢ ( 𝐴 = 𝐵 → ( Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶 ) ) |
9 | 5 8 | impbid | ⊢ ( 𝐴 = 𝐵 → ( Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶 ) ) |