Metamath Proof Explorer

Theorem disjeq1

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

Ref Expression
Assertion disjeq1 
|- ( A = B -> ( Disj_ x e. A C <-> Disj_ x e. B C ) )

Proof

Step Hyp Ref Expression
1 eqimss2 
 |-  ( A = B -> B C_ A )
2 disjss1 
 |-  ( B C_ A -> ( Disj_ x e. A C -> Disj_ x e. B C ) )
3 1 2 syl 
 |-  ( A = B -> ( Disj_ x e. A C -> Disj_ x e. B C ) )
4 eqimss 
 |-  ( A = B -> A C_ B )
5 disjss1 
 |-  ( A C_ B -> ( Disj_ x e. B C -> Disj_ x e. A C ) )
6 4 5 syl 
 |-  ( A = B -> ( Disj_ x e. B C -> Disj_ x e. A C ) )
7 3 6 impbid 
 |-  ( A = B -> ( Disj_ x e. A C <-> Disj_ x e. B C ) )