Metamath Proof Explorer


Theorem funimaexg

Description: Axiom of Replacement using abbreviations. Axiom 39(vi) of Quine p. 284. Compare Exercise 9 of TakeutiZaring p. 29. (Contributed by NM, 10-Sep-2006) Shorten proof and avoid ax-10 , ax-12 . (Revised by SN, 19-Dec-2024)

Ref Expression
Assertion funimaexg Fun A B C A B V

Proof

Step Hyp Ref Expression
1 dffun6 Fun A Rel A x * y x A y
2 1 simprbi Fun A x * y x A y
3 dfima2 A B = y | x B x A y
4 axrep6g B C x * y x A y y | x B x A y V
5 3 4 eqeltrid B C x * y x A y A B V
6 2 5 sylan2 B C Fun A A B V
7 6 ancoms Fun A B C A B V