Metamath Proof Explorer


Theorem dmfexALT

Description: Alternate proof of dmfex : shorter but using ax-rep . (Contributed by NM, 27-Aug-2006) (Proof shortened by Andrew Salmon, 17-Sep-2011) (Proof shortened by AV, 23-Aug-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dmfexALT
|- ( ( F e. C /\ F : A --> B ) -> A e. _V )

Proof

Step Hyp Ref Expression
1 elex
 |-  ( F e. C -> F e. _V )
2 fdmexb
 |-  ( F : A --> B -> ( A e. _V <-> F e. _V ) )
3 2 biimprd
 |-  ( F : A --> B -> ( F e. _V -> A e. _V ) )
4 1 3 mpan9
 |-  ( ( F e. C /\ F : A --> B ) -> A e. _V )