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 C F : A B A V

Proof

Step Hyp Ref Expression
1 elex F C F V
2 fdmexb F : A B A V F V
3 2 biimprd F : A B F V A V
4 1 3 mpan9 F C F : A B A V