Metamath Proof Explorer


Theorem dmoprab

Description: The domain of an operation class abstraction. (Contributed by NM, 17-Mar-1995) (Revised by David Abernethy, 19-Jun-2012)

Ref Expression
Assertion dmoprab
|- dom { <. <. x , y >. , z >. | ph } = { <. x , y >. | E. z ph }

Proof

Step Hyp Ref Expression
1 dfoprab2
 |-  { <. <. x , y >. , z >. | ph } = { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) }
2 1 dmeqi
 |-  dom { <. <. x , y >. , z >. | ph } = dom { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) }
3 dmopab
 |-  dom { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) } = { w | E. z E. x E. y ( w = <. x , y >. /\ ph ) }
4 exrot3
 |-  ( E. z E. x E. y ( w = <. x , y >. /\ ph ) <-> E. x E. y E. z ( w = <. x , y >. /\ ph ) )
5 19.42v
 |-  ( E. z ( w = <. x , y >. /\ ph ) <-> ( w = <. x , y >. /\ E. z ph ) )
6 5 2exbii
 |-  ( E. x E. y E. z ( w = <. x , y >. /\ ph ) <-> E. x E. y ( w = <. x , y >. /\ E. z ph ) )
7 4 6 bitri
 |-  ( E. z E. x E. y ( w = <. x , y >. /\ ph ) <-> E. x E. y ( w = <. x , y >. /\ E. z ph ) )
8 7 abbii
 |-  { w | E. z E. x E. y ( w = <. x , y >. /\ ph ) } = { w | E. x E. y ( w = <. x , y >. /\ E. z ph ) }
9 df-opab
 |-  { <. x , y >. | E. z ph } = { w | E. x E. y ( w = <. x , y >. /\ E. z ph ) }
10 8 9 eqtr4i
 |-  { w | E. z E. x E. y ( w = <. x , y >. /\ ph ) } = { <. x , y >. | E. z ph }
11 2 3 10 3eqtri
 |-  dom { <. <. x , y >. , z >. | ph } = { <. x , y >. | E. z ph }