Theorem dfiun2gOLD

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

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

Proof

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