Metamath Proof Explorer


Theorem funcsetcestrclem1

Description: Lemma 1 for funcsetcestrc . (Contributed by AV, 27-Mar-2020)

Ref Expression
Hypotheses funcsetcestrc.s S=SetCatU
funcsetcestrc.c C=BaseS
funcsetcestrc.f φF=xCBasendxx
Assertion funcsetcestrclem1 φXCFX=BasendxX

Proof

Step Hyp Ref Expression
1 funcsetcestrc.s S=SetCatU
2 funcsetcestrc.c C=BaseS
3 funcsetcestrc.f φF=xCBasendxx
4 3 adantr φXCF=xCBasendxx
5 opeq2 x=XBasendxx=BasendxX
6 5 sneqd x=XBasendxx=BasendxX
7 6 adantl φXCx=XBasendxx=BasendxX
8 simpr φXCXC
9 snex BasendxXV
10 9 a1i φXCBasendxXV
11 4 7 8 10 fvmptd φXCFX=BasendxX