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 A B Disj y A C

Proof

Step Hyp Ref Expression
1 cbvdisjv.1 x = y B = C
2 1 eleq2d x = y z B z C
3 2 cbvrmovw * x A z B * y A z C
4 3 albii z * x A z B z * y A z C
5 df-disj Disj x A B z * x A z B
6 df-disj Disj y A C z * y A z C
7 4 5 6 3bitr4i Disj x A B Disj y A C