This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑦 ∈ 𝐴 𝐶 )