Metamath Proof Explorer


Theorem fsets

Description: The structure replacement function is a function. (Contributed by SO, 12-Jul-2018)

Ref Expression
Assertion fsets FVF:ABXAYBFsSetXY:AB

Proof

Step Hyp Ref Expression
1 difss AXA
2 fssres F:ABAXAFAX:AXB
3 1 2 mpan2 F:ABFAX:AXB
4 ffn F:ABFFnA
5 fnresdm FFnAFA=F
6 4 5 syl F:ABFA=F
7 6 reseq1d F:ABFAVX=FVX
8 resres FAVX=FAVX
9 invdif AVX=AX
10 9 reseq2i FAVX=FAX
11 8 10 eqtri FAVX=FAX
12 7 11 eqtr3di F:ABFVX=FAX
13 12 feq1d F:ABFVX:AXBFAX:AXB
14 3 13 mpbird F:ABFVX:AXB
15 14 adantl FVF:ABFVX:AXB
16 fsnunf2 FVX:AXBXAYBFVXXY:AB
17 15 16 syl3an1 FVF:ABXAYBFVXXY:AB
18 simp1l FVF:ABXAYBFV
19 simp3 FVF:ABXAYBYB
20 setsval FVYBFsSetXY=FVXXY
21 20 feq1d FVYBFsSetXY:ABFVXXY:AB
22 18 19 21 syl2anc FVF:ABXAYBFsSetXY:ABFVXXY:AB
23 17 22 mpbird FVF:ABXAYBFsSetXY:AB