Theorem cbvdisj

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

	Ref	Expression
Hypotheses	cbvdisj.1	⊢ Ⅎ 𝑦 𝐵
	cbvdisj.2	⊢ Ⅎ 𝑥 𝐶
	cbvdisj.3	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
Assertion	cbvdisj	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		cbvdisj.1	⊢ Ⅎ 𝑦 𝐵
2		cbvdisj.2	⊢ Ⅎ 𝑥 𝐶
3		cbvdisj.3	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
4	1	nfcri	⊢ Ⅎ 𝑦 𝑧 ∈ 𝐵
5	2	nfcri	⊢ Ⅎ 𝑥 𝑧 ∈ 𝐶
6	3	eleq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶 ) )
7	4 5 6	cbvrmow	⊢ ( ∃* 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃* 𝑦 ∈ 𝐴 𝑧 ∈ 𝐶 )
8	7	albii	⊢ ( ∀ 𝑧 ∃* 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∀ 𝑧 ∃* 𝑦 ∈ 𝐴 𝑧 ∈ 𝐶 )
9		df-disj	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑧 ∃* 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 )
10		df-disj	⊢ ( Disj 𝑦 ∈ 𝐴 𝐶 ↔ ∀ 𝑧 ∃* 𝑦 ∈ 𝐴 𝑧 ∈ 𝐶 )
11	8 9 10	3bitr4i	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶 )