Metamath Proof Explorer


Theorem disjeq1f

Description: Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016)

Ref Expression
Hypotheses disjss1f.1 𝑥 𝐴
disjss1f.2 𝑥 𝐵
Assertion disjeq1f ( 𝐴 = 𝐵 → ( Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ) )

Proof

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 𝑥𝐵 𝐶 ) )