Metamath Proof Explorer

Theorem dfco2

Description: Alternate definition of a class composition, using only one bound variable. (Contributed by NM, 19-Dec-2008)

Ref Expression
Assertion dfco2 
|- ( A o. B ) = U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) )

Proof

Step Hyp Ref Expression
1 relco 
 |-  Rel ( A o. B )
2 reliun 
 |-  ( Rel U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) ) <-> A. x e. _V Rel ( ( `' B " { x } ) X. ( A " { x } ) ) )
3 relxp 
 |-  Rel ( ( `' B " { x } ) X. ( A " { x } ) )
4 3 a1i 
 |-  ( x e. _V -> Rel ( ( `' B " { x } ) X. ( A " { x } ) ) )
5 2 4 mprgbir 
 |-  Rel U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) )
6 opelco2g 
 |-  ( ( y e. _V /\ z e. _V ) -> ( <. y , z >. e. ( A o. B ) <-> E. x ( <. y , x >. e. B /\ <. x , z >. e. A ) ) )
7 6 el2v 
 |-  ( <. y , z >. e. ( A o. B ) <-> E. x ( <. y , x >. e. B /\ <. x , z >. e. A ) )
8 eliun 
 |-  ( <. y , z >. e. U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) ) <-> E. x e. _V <. y , z >. e. ( ( `' B " { x } ) X. ( A " { x } ) ) )
9 rexv 
 |-  ( E. x e. _V <. y , z >. e. ( ( `' B " { x } ) X. ( A " { x } ) ) <-> E. x <. y , z >. e. ( ( `' B " { x } ) X. ( A " { x } ) ) )
10 opelxp 
 |-  ( <. y , z >. e. ( ( `' B " { x } ) X. ( A " { x } ) ) <-> ( y e. ( `' B " { x } ) /\ z e. ( A " { x } ) ) )
11 vex 
 |-  x e. _V
12 vex 
 |-  y e. _V
13 11 12 elimasn 
 |-  ( y e. ( `' B " { x } ) <-> <. x , y >. e. `' B )
14 11 12 opelcnv 
 |-  ( <. x , y >. e. `' B <-> <. y , x >. e. B )
15 13 14 bitri 
 |-  ( y e. ( `' B " { x } ) <-> <. y , x >. e. B )
16 vex 
 |-  z e. _V
17 11 16 elimasn 
 |-  ( z e. ( A " { x } ) <-> <. x , z >. e. A )
18 15 17 anbi12i 
 |-  ( ( y e. ( `' B " { x } ) /\ z e. ( A " { x } ) ) <-> ( <. y , x >. e. B /\ <. x , z >. e. A ) )
19 10 18 bitri 
 |-  ( <. y , z >. e. ( ( `' B " { x } ) X. ( A " { x } ) ) <-> ( <. y , x >. e. B /\ <. x , z >. e. A ) )
20 19 exbii 
 |-  ( E. x <. y , z >. e. ( ( `' B " { x } ) X. ( A " { x } ) ) <-> E. x ( <. y , x >. e. B /\ <. x , z >. e. A ) )
21 8 9 20 3bitrri 
 |-  ( E. x ( <. y , x >. e. B /\ <. x , z >. e. A ) <-> <. y , z >. e. U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) ) )
22 7 21 bitri 
 |-  ( <. y , z >. e. ( A o. B ) <-> <. y , z >. e. U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) ) )
23 1 5 22 eqrelriiv 
 |-  ( A o. B ) = U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) )