Metamath Proof Explorer


Theorem oprabrexex2

Description: Existence of an existentially restricted operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010)

Ref Expression
Hypotheses oprabrexex2.1 A V
oprabrexex2.2 x y z | φ V
Assertion oprabrexex2 x y z | w A φ V

Proof

Step Hyp Ref Expression
1 oprabrexex2.1 A V
2 oprabrexex2.2 x y z | φ V
3 df-oprab x y z | w A φ = v | x y z v = x y z w A φ
4 rexcom4 w A x y z v = x y z φ x w A y z v = x y z φ
5 rexcom4 w A y z v = x y z φ y w A z v = x y z φ
6 rexcom4 w A z v = x y z φ z w A v = x y z φ
7 r19.42v w A v = x y z φ v = x y z w A φ
8 7 exbii z w A v = x y z φ z v = x y z w A φ
9 6 8 bitri w A z v = x y z φ z v = x y z w A φ
10 9 exbii y w A z v = x y z φ y z v = x y z w A φ
11 5 10 bitri w A y z v = x y z φ y z v = x y z w A φ
12 11 exbii x w A y z v = x y z φ x y z v = x y z w A φ
13 4 12 bitr2i x y z v = x y z w A φ w A x y z v = x y z φ
14 13 abbii v | x y z v = x y z w A φ = v | w A x y z v = x y z φ
15 3 14 eqtri x y z | w A φ = v | w A x y z v = x y z φ
16 df-oprab x y z | φ = v | x y z v = x y z φ
17 16 2 eqeltrri v | x y z v = x y z φ V
18 1 17 abrexex2 v | w A x y z v = x y z φ V
19 15 18 eqeltri x y z | w A φ V