Theorem abrexco

Description: Composition of two image maps C ( y ) and B ( w ) . (Contributed by NM, 27-May-2013)

	Ref	Expression
Hypotheses	abrexco.1	⊢ 𝐵 ∈ V
	abrexco.2	⊢ ( 𝑦 = 𝐵 → 𝐶 = 𝐷 )
Assertion	abrexco	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ 𝐴 𝑧 = 𝐵 } 𝑥 = 𝐶 } = { 𝑥 ∣ ∃ 𝑤 ∈ 𝐴 𝑥 = 𝐷 }

Proof

Step	Hyp	Ref	Expression
1		abrexco.1	⊢ 𝐵 ∈ V
2		abrexco.2	⊢ ( 𝑦 = 𝐵 → 𝐶 = 𝐷 )
3		df-rex	⊢ ( ∃ 𝑦 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ 𝐴 𝑧 = 𝐵 } 𝑥 = 𝐶 ↔ ∃ 𝑦 ( 𝑦 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ 𝐴 𝑧 = 𝐵 } ∧ 𝑥 = 𝐶 ) )
4		vex	⊢ 𝑦 ∈ V
5		eqeq1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 = 𝐵 ↔ 𝑦 = 𝐵 ) )
6	5	rexbidv	⊢ ( 𝑧 = 𝑦 → ( ∃ 𝑤 ∈ 𝐴 𝑧 = 𝐵 ↔ ∃ 𝑤 ∈ 𝐴 𝑦 = 𝐵 ) )
7	4 6	elab	⊢ ( 𝑦 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ 𝐴 𝑧 = 𝐵 } ↔ ∃ 𝑤 ∈ 𝐴 𝑦 = 𝐵 )
8	7	anbi1i	⊢ ( ( 𝑦 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ 𝐴 𝑧 = 𝐵 } ∧ 𝑥 = 𝐶 ) ↔ ( ∃ 𝑤 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑥 = 𝐶 ) )
9		r19.41v	⊢ ( ∃ 𝑤 ∈ 𝐴 ( 𝑦 = 𝐵 ∧ 𝑥 = 𝐶 ) ↔ ( ∃ 𝑤 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑥 = 𝐶 ) )
10	8 9	bitr4i	⊢ ( ( 𝑦 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ 𝐴 𝑧 = 𝐵 } ∧ 𝑥 = 𝐶 ) ↔ ∃ 𝑤 ∈ 𝐴 ( 𝑦 = 𝐵 ∧ 𝑥 = 𝐶 ) )
11	10	exbii	⊢ ( ∃ 𝑦 ( 𝑦 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ 𝐴 𝑧 = 𝐵 } ∧ 𝑥 = 𝐶 ) ↔ ∃ 𝑦 ∃ 𝑤 ∈ 𝐴 ( 𝑦 = 𝐵 ∧ 𝑥 = 𝐶 ) )
12	3 11	bitri	⊢ ( ∃ 𝑦 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ 𝐴 𝑧 = 𝐵 } 𝑥 = 𝐶 ↔ ∃ 𝑦 ∃ 𝑤 ∈ 𝐴 ( 𝑦 = 𝐵 ∧ 𝑥 = 𝐶 ) )
13		rexcom4	⊢ ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑥 = 𝐶 ) ↔ ∃ 𝑦 ∃ 𝑤 ∈ 𝐴 ( 𝑦 = 𝐵 ∧ 𝑥 = 𝐶 ) )
14	12 13	bitr4i	⊢ ( ∃ 𝑦 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ 𝐴 𝑧 = 𝐵 } 𝑥 = 𝐶 ↔ ∃ 𝑤 ∈ 𝐴 ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑥 = 𝐶 ) )
15	2	eqeq2d	⊢ ( 𝑦 = 𝐵 → ( 𝑥 = 𝐶 ↔ 𝑥 = 𝐷 ) )
16	1 15	ceqsexv	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑥 = 𝐶 ) ↔ 𝑥 = 𝐷 )
17	16	rexbii	⊢ ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑥 = 𝐶 ) ↔ ∃ 𝑤 ∈ 𝐴 𝑥 = 𝐷 )
18	14 17	bitri	⊢ ( ∃ 𝑦 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ 𝐴 𝑧 = 𝐵 } 𝑥 = 𝐶 ↔ ∃ 𝑤 ∈ 𝐴 𝑥 = 𝐷 )
19	18	abbii	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ 𝐴 𝑧 = 𝐵 } 𝑥 = 𝐶 } = { 𝑥 ∣ ∃ 𝑤 ∈ 𝐴 𝑥 = 𝐷 }