Metamath Proof Explorer


Theorem mpo2eqb

Description: Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnov2 . (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Assertion mpo2eqb x A y B C V x A , y B C = x A , y B D x A y B C = D

Proof

Step Hyp Ref Expression
1 df-mpo x A , y B C = x y z | x A y B z = C
2 df-mpo x A , y B D = x y z | x A y B z = D
3 1 2 eqeq12i x A , y B C = x A , y B D x y z | x A y B z = C = x y z | x A y B z = D
4 eqoprab2bw x y z | x A y B z = C = x y z | x A y B z = D x y z x A y B z = C x A y B z = D
5 pm5.32 x A y B z = C z = D x A y B z = C x A y B z = D
6 5 albii z x A y B z = C z = D z x A y B z = C x A y B z = D
7 19.21v z x A y B z = C z = D x A y B z z = C z = D
8 6 7 bitr3i z x A y B z = C x A y B z = D x A y B z z = C z = D
9 8 2albii x y z x A y B z = C x A y B z = D x y x A y B z z = C z = D
10 r2al x A y B z z = C z = D x y x A y B z z = C z = D
11 9 10 bitr4i x y z x A y B z = C x A y B z = D x A y B z z = C z = D
12 3 4 11 3bitri x A , y B C = x A , y B D x A y B z z = C z = D
13 pm13.183 C V C = D z z = C z = D
14 13 ralimi y B C V y B C = D z z = C z = D
15 ralbi y B C = D z z = C z = D y B C = D y B z z = C z = D
16 14 15 syl y B C V y B C = D y B z z = C z = D
17 16 ralimi x A y B C V x A y B C = D y B z z = C z = D
18 ralbi x A y B C = D y B z z = C z = D x A y B C = D x A y B z z = C z = D
19 17 18 syl x A y B C V x A y B C = D x A y B z z = C z = D
20 12 19 bitr4id x A y B C V x A , y B C = x A , y B D x A y B C = D