Theorem cbvdisjv 5068

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

Hypothesis

Ref	Expression
cbvdisjv.1	⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)

Assertion

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

Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶

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

Proof of Theorem cbvdisjv

Step	Hyp	Ref	Expression
1		nfcv 2904	. 2 ⊢ Ⅎ𝑦𝐵
2		nfcv 2904	. 2 ⊢ Ⅎ𝑥𝐶
3		cbvdisjv.1	. 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
4	1, 2, 3	cbvdisj 5067	1 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540  Disj wdisj 5057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-11 2153  ax-12 2170  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-ex 1781  df-nf 1785  df-mo 2538  df-cleq 2728  df-clel 2814  df-nfc 2886  df-rmo 3349  df-disj 5058

This theorem is referenced by:  uniioombllem4  24856  hashunif  31413  tocyccntz  31698  totprob  32694  disjrnmpt2  43061  ismeannd  44350  psmeasure  44354  volmea  44357  meaiuninclem  44363  caratheodorylem1  44409  caratheodory  44411