Metamath Proof Explorer


Theorem fsn2

Description: A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by NM, 19-May-2004)

Ref Expression
Hypothesis fsn2.1 A V
Assertion fsn2 F : A B F A B F = A F A

Proof

Step Hyp Ref Expression
1 fsn2.1 A V
2 1 snid A A
3 ffvelrn F : A B A A F A B
4 2 3 mpan2 F : A B F A B
5 ffn F : A B F Fn A
6 dffn3 F Fn A F : A ran F
7 6 biimpi F Fn A F : A ran F
8 imadmrn F dom F = ran F
9 fndm F Fn A dom F = A
10 9 imaeq2d F Fn A F dom F = F A
11 8 10 eqtr3id F Fn A ran F = F A
12 fnsnfv F Fn A A A F A = F A
13 2 12 mpan2 F Fn A F A = F A
14 11 13 eqtr4d F Fn A ran F = F A
15 14 feq3d F Fn A F : A ran F F : A F A
16 7 15 mpbid F Fn A F : A F A
17 5 16 syl F : A B F : A F A
18 4 17 jca F : A B F A B F : A F A
19 snssi F A B F A B
20 fss F : A F A F A B F : A B
21 20 ancoms F A B F : A F A F : A B
22 19 21 sylan F A B F : A F A F : A B
23 18 22 impbii F : A B F A B F : A F A
24 fvex F A V
25 1 24 fsn F : A F A F = A F A
26 25 anbi2i F A B F : A F A F A B F = A F A
27 23 26 bitri F : A B F A B F = A F A