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 ) }