Metamath Proof Explorer

Theorem funimaexgOLD

Description: Obsolete version of funimaexg as of 19-Dec-2024. (Contributed by NM, 10-Sep-2006) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion funimaexgOLD ⊢Fun⁡A∧B∈C→AB∈V

Proof

Step Hyp Ref Expression
1 imaeq2 ⊢w=B→Aw=AB
2 1 eleq1d ⊢w=B→Aw∈V↔AB∈V
3 2 imbi2d ⊢w=B→Fun⁡A→Aw∈V↔Fun⁡A→AB∈V
4 dffun5 ⊢Fun⁡A↔Rel⁡A∧∀x∃z∀yxy∈A→y=z
5 nfv ⊢Ⅎzxy∈A
6 5 axrep4 ⊢∀x∃z∀yxy∈A→y=z→∃z∀yy∈z↔∃xx∈w∧xy∈A
7 isset ⊢Aw∈V↔∃zz=Aw
8 dfima3 ⊢Aw=y|∃xx∈w∧xy∈A
9 8 eqeq2i ⊢z=Aw↔z=y|∃xx∈w∧xy∈A
10 eqabb ⊢z=y|∃xx∈w∧xy∈A↔∀yy∈z↔∃xx∈w∧xy∈A
11 9 10 bitri ⊢z=Aw↔∀yy∈z↔∃xx∈w∧xy∈A
12 11 exbii ⊢∃zz=Aw↔∃z∀yy∈z↔∃xx∈w∧xy∈A
13 7 12 bitri ⊢Aw∈V↔∃z∀yy∈z↔∃xx∈w∧xy∈A
14 6 13 sylibr ⊢∀x∃z∀yxy∈A→y=z→Aw∈V
15 4 14 simplbiim ⊢Fun⁡A→Aw∈V
16 3 15 vtoclg ⊢B∈C→Fun⁡A→AB∈V
17 16 impcom ⊢Fun⁡A∧B∈C→AB∈V