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 ( 𝑥 = 𝑦𝐵 = 𝐶 )
Assertion cbvdisjv ( Disj 𝑥𝐴 𝐵Disj 𝑦𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 cbvdisjv.1 ( 𝑥 = 𝑦𝐵 = 𝐶 )
2 1 eleq2d ( 𝑥 = 𝑦 → ( 𝑧𝐵𝑧𝐶 ) )
3 2 cbvrmovw ( ∃* 𝑥𝐴 𝑧𝐵 ↔ ∃* 𝑦𝐴 𝑧𝐶 )
4 3 albii ( ∀ 𝑧 ∃* 𝑥𝐴 𝑧𝐵 ↔ ∀ 𝑧 ∃* 𝑦𝐴 𝑧𝐶 )
5 df-disj ( Disj 𝑥𝐴 𝐵 ↔ ∀ 𝑧 ∃* 𝑥𝐴 𝑧𝐵 )
6 df-disj ( Disj 𝑦𝐴 𝐶 ↔ ∀ 𝑧 ∃* 𝑦𝐴 𝑧𝐶 )
7 4 5 6 3bitr4i ( Disj 𝑥𝐴 𝐵Disj 𝑦𝐴 𝐶 )