Metamath Proof Explorer

Theorem cnvimadfsn

Description: The support of functions "defined" by inverse images expressed by binary relations. (Contributed by AV, 7-Apr-2019)

Ref Expression
Assertion cnvimadfsn 
|- ( `' R " ( _V \ { Z } ) ) = { x | E. y ( x R y /\ y =/= Z ) }

Proof

Step Hyp Ref Expression
1 dfima3 
 |-  ( `' R " ( _V \ { Z } ) ) = { x | E. y ( y e. ( _V \ { Z } ) /\ <. y , x >. e. `' R ) }
2 eldifvsn 
 |-  ( y e. _V -> ( y e. ( _V \ { Z } ) <-> y =/= Z ) )
3 2 elv 
 |-  ( y e. ( _V \ { Z } ) <-> y =/= Z )
4 vex 
 |-  y e. _V
5 vex 
 |-  x e. _V
6 4 5 opelcnv 
 |-  ( <. y , x >. e. `' R <-> <. x , y >. e. R )
7 df-br 
 |-  ( x R y <-> <. x , y >. e. R )
8 6 7 bitr4i 
 |-  ( <. y , x >. e. `' R <-> x R y )
9 3 8 anbi12ci 
 |-  ( ( y e. ( _V \ { Z } ) /\ <. y , x >. e. `' R ) <-> ( x R y /\ y =/= Z ) )
10 9 exbii 
 |-  ( E. y ( y e. ( _V \ { Z } ) /\ <. y , x >. e. `' R ) <-> E. y ( x R y /\ y =/= Z ) )
11 10 abbii 
 |-  { x | E. y ( y e. ( _V \ { Z } ) /\ <. y , x >. e. `' R ) } = { x | E. y ( x R y /\ y =/= Z ) }
12 1 11 eqtri 
 |-  ( `' R " ( _V \ { Z } ) ) = { x | E. y ( x R y /\ y =/= Z ) }