Theorem cbvdisj 3916

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

Hypotheses

Ref	Expression
cbvdisj.1	⊢ Ⅎ𝑦𝐵
cbvdisj.2	⊢ Ⅎ𝑥𝐶
cbvdisj.3	⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)

Assertion

Ref	Expression
cbvdisj	⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶)

Distinct variable group:   𝑥,𝑦,𝐴

Allowed substitution hints:   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)

Proof of Theorem cbvdisj

Dummy variable 𝑧 is distinct from all other variables.

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

Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1329   = wceq 1331   ∈ wcel 1480  Ⅎwnfc 2268  ∃*wrmo 2419  Disj wdisj 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rex 2422  df-reu 2423  df-rmo 2424  df-disj 3907

This theorem is referenced by:  cbvdisjv  3917  disjnims  3921