Metamath Proof Explorer

Theorem rncoOLD

Description: Obsolete version of rnco as of 24-Jan-2026. (Contributed by NM, 12-Dec-2006) (Proof shortened by Peter Mazsa, 2-Oct-2022) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion rncoOLD ⊢ ran ⁡ A ∘ B = ran ⁡ A ↾ ran ⁡ B

Proof

Step Hyp Ref Expression
1 vex ⊢ x ∈ V
2 vex ⊢ y ∈ V
3 1 2 brco ⊢ x A ∘ B y ↔ ∃ z x B z ∧ z A y
4 3 exbii ⊢ ∃ x x A ∘ B y ↔ ∃ x ∃ z x B z ∧ z A y
5 excom ⊢ ∃ x ∃ z x B z ∧ z A y ↔ ∃ z ∃ x x B z ∧ z A y
6 vex ⊢ z ∈ V
7 6 elrn ⊢ z ∈ ran ⁡ B ↔ ∃ x x B z
8 7 anbi1i ⊢ z ∈ ran ⁡ B ∧ z A y ↔ ∃ x x B z ∧ z A y
9 2 brresi ⊢ z A ↾ ran ⁡ B y ↔ z ∈ ran ⁡ B ∧ z A y
10 19.41v ⊢ ∃ x x B z ∧ z A y ↔ ∃ x x B z ∧ z A y
11 8 9 10 3bitr4ri ⊢ ∃ x x B z ∧ z A y ↔ z A ↾ ran ⁡ B y
12 11 exbii ⊢ ∃ z ∃ x x B z ∧ z A y ↔ ∃ z z A ↾ ran ⁡ B y
13 4 5 12 3bitri ⊢ ∃ x x A ∘ B y ↔ ∃ z z A ↾ ran ⁡ B y
14 2 elrn ⊢ y ∈ ran ⁡ A ∘ B ↔ ∃ x x A ∘ B y
15 2 elrn ⊢ y ∈ ran ⁡ A ↾ ran ⁡ B ↔ ∃ z z A ↾ ran ⁡ B y
16 13 14 15 3bitr4i ⊢ y ∈ ran ⁡ A ∘ B ↔ y ∈ ran ⁡ A ↾ ran ⁡ B
17 16 eqriv ⊢ ran ⁡ A ∘ B = ran ⁡ A ↾ ran ⁡ B