Metamath Proof Explorer


Theorem bj-opabco

Description: Composition of ordered-pair class abstractions. (Contributed by BJ, 22-May-2024)

Ref Expression
Assertion bj-opabco y z | ψ x y | φ = x z | y φ ψ

Proof

Step Hyp Ref Expression
1 df-co y z | ψ x y | φ = a b | c a x y | φ c c y z | ψ b
2 nfcv _ x a
3 nfopab1 _ x x y | φ
4 nfcv _ x c
5 2 3 4 nfbr x a x y | φ c
6 nfv x c y z | ψ b
7 5 6 nfan x a x y | φ c c y z | ψ b
8 7 nfex x c a x y | φ c c y z | ψ b
9 nfv z a x y | φ c
10 nfcv _ z c
11 nfopab2 _ z y z | ψ
12 nfcv _ z b
13 10 11 12 nfbr z c y z | ψ b
14 9 13 nfan z a x y | φ c c y z | ψ b
15 14 nfex z c a x y | φ c c y z | ψ b
16 nfv a y x x y | φ y y y z | ψ z
17 nfv b y x x y | φ y y y z | ψ z
18 nfv y a = x b = z
19 nfcv _ y a
20 nfopab2 _ y x y | φ
21 nfcv _ y c
22 19 20 21 nfbr y a x y | φ c
23 nfopab1 _ y y z | ψ
24 nfcv _ y b
25 21 23 24 nfbr y c y z | ψ b
26 22 25 nfan y a x y | φ c c y z | ψ b
27 26 a1i a = x b = z y a x y | φ c c y z | ψ b
28 simpll a = x b = z c = y a = x
29 simpr a = x b = z c = y c = y
30 28 29 breq12d a = x b = z c = y a x y | φ c x x y | φ y
31 simplr a = x b = z c = y b = z
32 29 31 breq12d a = x b = z c = y c y z | ψ b y y z | ψ z
33 30 32 anbi12d a = x b = z c = y a x y | φ c c y z | ψ b x x y | φ y y y z | ψ z
34 33 ex a = x b = z c = y a x y | φ c c y z | ψ b x x y | φ y y y z | ψ z
35 18 27 34 cbvexdw a = x b = z c a x y | φ c c y z | ψ b y x x y | φ y y y z | ψ z
36 8 15 16 17 35 cbvopab a b | c a x y | φ c c y z | ψ b = x z | y x x y | φ y y y z | ψ z
37 bj-opelopabid x x y | φ y φ
38 bj-opelopabid y y z | ψ z ψ
39 37 38 anbi12i x x y | φ y y y z | ψ z φ ψ
40 39 exbii y x x y | φ y y y z | ψ z y φ ψ
41 40 opabbii x z | y x x y | φ y y y z | ψ z = x z | y φ ψ
42 1 36 41 3eqtri y z | ψ x y | φ = x z | y φ ψ