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