This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem disjeq2

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

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

Proof

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