Metamath Proof Explorer


Theorem funop1

Description: A function is an ordered pair iff it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020)

Ref Expression
Assertion funop1 x y F = x y Fun F x y F = x y

Proof

Step Hyp Ref Expression
1 opeq12 x = v y = w x y = v w
2 1 eqeq2d x = v y = w F = x y F = v w
3 2 cbvex2vw x y F = x y v w F = v w
4 vex v V
5 vex w V
6 4 5 funopsn Fun F F = v w a v = a F = a a
7 vex a V
8 opeq12 x = a y = a x y = a a
9 8 sneqd x = a y = a x y = a a
10 9 eqeq2d x = a y = a F = x y F = a a
11 7 7 10 spc2ev F = a a x y F = x y
12 11 adantl v = a F = a a x y F = x y
13 12 exlimiv a v = a F = a a x y F = x y
14 6 13 syl Fun F F = v w x y F = x y
15 14 expcom F = v w Fun F x y F = x y
16 vex x V
17 vex y V
18 16 17 funsn Fun x y
19 funeq F = x y Fun F Fun x y
20 18 19 mpbiri F = x y Fun F
21 20 exlimivv x y F = x y Fun F
22 15 21 impbid1 F = v w Fun F x y F = x y
23 22 exlimivv v w F = v w Fun F x y F = x y
24 3 23 sylbi x y F = x y Fun F x y F = x y