csbuni

Description: Distribute proper substitution through the union of a class. (Contributed by Alan Sare, 10-Nov-2012) (Revised by NM, 22-Aug-2018)

		Ref	Expression
	Assertion	csbuni	⊢ ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = ∪ ⦋ 𝐴 / 𝑥 ⦌ 𝐵

Proof

Step	Hyp	Ref	Expression
1		csbab	⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } = { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) }
2		sbcex2	⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) )
3		sbcan	⊢ ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ) )
4		sbcg	⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦 ) )
5	4	anbi1d	⊢ ( 𝐴 ∈ V → ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝑦 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ) ) )
6		sbcel2	⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
7	6	anbi2i	⊢ ( ( 𝑧 ∈ 𝑦 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
8	5 7	bitrdi	⊢ ( 𝐴 ∈ V → ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) )
9	3 8	bitrid	⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) )
10	9	exbidv	⊢ ( 𝐴 ∈ V → ( ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) )
11	2 10	bitrid	⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) )
12	11	abbidv	⊢ ( 𝐴 ∈ V → { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) } )
13	1 12	eqtrid	⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) } )
14		df-uni	⊢ ∪ 𝐵 = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) }
15	14	csbeq2i	⊢ ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) }
16		df-uni	⊢ ∪ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) }
17	13 15 16	3eqtr4g	⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = ∪ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
18		csbprc	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = ∅ )
19		csbprc	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ∅ )
20	19	unieqd	⊢ ( ¬ 𝐴 ∈ V → ∪ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ∪ ∅ )
21		uni0	⊢ ∪ ∅ = ∅
22	20 21	eqtr2di	⊢ ( ¬ 𝐴 ∈ V → ∅ = ∪ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
23	18 22	eqtrd	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = ∪ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
24	17 23	pm2.61i	⊢ ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = ∪ ⦋ 𝐴 / 𝑥 ⦌ 𝐵

Metamath Proof Explorer

Theorem csbuni

Proof