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 }