Metamath Proof Explorer

Theorem elunirn2OLD

Description: Obsolete version of elfvunirn as of 12-Jan-2025. (Contributed by Thierry Arnoux, 13-Nov-2016) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion elunirn2OLD 
|- ( ( Fun F /\ B e. ( F ` A ) ) -> B e. U. ran F )

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( B e. ( F ` A ) -> A e. dom F )
2 fveq2 
 |-  ( x = A -> ( F ` x ) = ( F ` A ) )
3 2 eleq2d 
 |-  ( x = A -> ( B e. ( F ` x ) <-> B e. ( F ` A ) ) )
4 3 rspcev 
 |-  ( ( A e. dom F /\ B e. ( F ` A ) ) -> E. x e. dom F B e. ( F ` x ) )
5 1 4 mpancom 
 |-  ( B e. ( F ` A ) -> E. x e. dom F B e. ( F ` x ) )
6 5 adantl 
 |-  ( ( Fun F /\ B e. ( F ` A ) ) -> E. x e. dom F B e. ( F ` x ) )
7 elunirn 
 |-  ( Fun F -> ( B e. U. ran F <-> E. x e. dom F B e. ( F ` x ) ) )
8 7 adantr 
 |-  ( ( Fun F /\ B e. ( F ` A ) ) -> ( B e. U. ran F <-> E. x e. dom F B e. ( F ` x ) ) )
9 6 8 mpbird 
 |-  ( ( Fun F /\ B e. ( F ` A ) ) -> B e. U. ran F )