Metamath Proof Explorer

Theorem abrexco

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

Ref Expression
Hypotheses abrexco.1 ⊢ B ∈ V
abrexco.2 ⊢ y = B → C = D
Assertion abrexco ⊢ x | ∃ y ∈ z | ∃ w ∈ A z = B x = C = x | ∃ w ∈ A x = D

Proof

Step Hyp Ref Expression
1 abrexco.1 ⊢ B ∈ V
2 abrexco.2 ⊢ y = B → C = D
3 df-rex ⊢ ∃ y ∈ z | ∃ w ∈ A z = B x = C ↔ ∃ y y ∈ z | ∃ w ∈ A z = B ∧ x = C
4 vex ⊢ y ∈ V
5 eqeq1 ⊢ z = y → z = B ↔ y = B
6 5 rexbidv ⊢ z = y → ∃ w ∈ A z = B ↔ ∃ w ∈ A y = B
7 4 6 elab ⊢ y ∈ z | ∃ w ∈ A z = B ↔ ∃ w ∈ A y = B
8 7 anbi1i ⊢ y ∈ z | ∃ w ∈ A z = B ∧ x = C ↔ ∃ w ∈ A y = B ∧ x = C
9 r19.41v ⊢ ∃ w ∈ A y = B ∧ x = C ↔ ∃ w ∈ A y = B ∧ x = C
10 8 9 bitr4i ⊢ y ∈ z | ∃ w ∈ A z = B ∧ x = C ↔ ∃ w ∈ A y = B ∧ x = C
11 10 exbii ⊢ ∃ y y ∈ z | ∃ w ∈ A z = B ∧ x = C ↔ ∃ y ∃ w ∈ A y = B ∧ x = C
12 3 11 bitri ⊢ ∃ y ∈ z | ∃ w ∈ A z = B x = C ↔ ∃ y ∃ w ∈ A y = B ∧ x = C
13 rexcom4 ⊢ ∃ w ∈ A ∃ y y = B ∧ x = C ↔ ∃ y ∃ w ∈ A y = B ∧ x = C
14 12 13 bitr4i ⊢ ∃ y ∈ z | ∃ w ∈ A z = B x = C ↔ ∃ w ∈ A ∃ y y = B ∧ x = C
15 2 eqeq2d ⊢ y = B → x = C ↔ x = D
16 1 15 ceqsexv ⊢ ∃ y y = B ∧ x = C ↔ x = D
17 16 rexbii ⊢ ∃ w ∈ A ∃ y y = B ∧ x = C ↔ ∃ w ∈ A x = D
18 14 17 bitri ⊢ ∃ y ∈ z | ∃ w ∈ A z = B x = C ↔ ∃ w ∈ A x = D
19 18 abbii ⊢ x | ∃ y ∈ z | ∃ w ∈ A z = B x = C = x | ∃ w ∈ A x = D