Metamath Proof Explorer

Theorem cbvdisjv

Description: Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 11-Dec-2016)

Ref Expression
Hypothesis cbvdisjv.1 
|- ( x = y -> B = C )
Assertion cbvdisjv 
|- ( Disj_ x e. A B <-> Disj_ y e. A C )

Proof

Step Hyp Ref Expression
1 cbvdisjv.1 
 |-  ( x = y -> B = C )
2 nfcv 
 |-  F/_ y B
3 nfcv 
 |-  F/_ x C
4 2 3 1 cbvdisj 
 |-  ( Disj_ x e. A B <-> Disj_ y e. A C )