Theorem cbvdisjf

Description: Change bound variables in a disjoint collection. (Contributed by Thierry Arnoux, 6-Apr-2017)

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

Proof

Step	Hyp	Ref	Expression
1		cbvdisjf.1	⊢ Ⅎ 𝑥 𝐴
2		cbvdisjf.2	⊢ Ⅎ 𝑦 𝐵
3		cbvdisjf.3	⊢ Ⅎ 𝑥 𝐶
4		cbvdisjf.4	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
5		nfv	⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
6	2	nfcri	⊢ Ⅎ 𝑦 𝑧 ∈ 𝐵
7	5 6	nfan	⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 )
8	1	nfcri	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
9	3	nfcri	⊢ Ⅎ 𝑥 𝑧 ∈ 𝐶
10	8 9	nfan	⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 )
11		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
12	4	eleq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶 ) )
13	11 12	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) )
14	7 10 13	cbvmow	⊢ ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ↔ ∃* 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) )
15		df-rmo	⊢ ( ∃* 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) )
16		df-rmo	⊢ ( ∃* 𝑦 ∈ 𝐴 𝑧 ∈ 𝐶 ↔ ∃* 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) )
17	14 15 16	3bitr4i	⊢ ( ∃* 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃* 𝑦 ∈ 𝐴 𝑧 ∈ 𝐶 )
18	17	albii	⊢ ( ∀ 𝑧 ∃* 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∀ 𝑧 ∃* 𝑦 ∈ 𝐴 𝑧 ∈ 𝐶 )
19		df-disj	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑧 ∃* 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 )
20		df-disj	⊢ ( Disj 𝑦 ∈ 𝐴 𝐶 ↔ ∀ 𝑧 ∃* 𝑦 ∈ 𝐴 𝑧 ∈ 𝐶 )
21	18 19 20	3bitr4i	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶 )