Theorem dfiun2gOLD

Description: Obsolete version of dfiun2g as of 11-Dec-2024. (Contributed by NM, 23-Mar-2006) (Proof shortened by Andrew Salmon, 25-Jul-2011) (Proof shortened by Rohan Ridenour, 11-Aug-2023) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	dfiun2gOLD	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶
2		rspa	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
3		clel3g	⊢ ( 𝐵 ∈ 𝐶 → ( 𝑧 ∈ 𝐵 ↔ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦 ) ) )
4	2 3	syl	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑧 ∈ 𝐵 ↔ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦 ) ) )
5	1 4	rexbida	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦 ) ) )
6		rexcom4	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 ( 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦 ) )
7	5 6	bitrdi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 ( 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦 ) ) )
8		r19.41v	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦 ) )
9	8	exbii	⊢ ( ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 ( 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑦 ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦 ) )
10		exancom	⊢ ( ∃ 𝑦 ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ) )
11	9 10	bitri	⊢ ( ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 ( 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ) )
12	7 11	bitrdi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ) ) )
13		eliun	⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 )
14		eluniab	⊢ ( 𝑧 ∈ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ↔ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ) )
15	12 13 14	3bitr4g	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑧 ∈ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ) )
16	15	eqrdv	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )