Metamath Proof Explorer


Theorem ressunif

Description: UnifSet is unaffected by restriction. (Contributed by Thierry Arnoux, 7-Dec-2017)

Ref Expression
Hypotheses ressunif.1 𝐻 = ( 𝐺s 𝐴 )
ressunif.2 𝑈 = ( UnifSet ‘ 𝐺 )
Assertion ressunif ( 𝐴𝑉𝑈 = ( UnifSet ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 ressunif.1 𝐻 = ( 𝐺s 𝐴 )
2 ressunif.2 𝑈 = ( UnifSet ‘ 𝐺 )
3 unifid UnifSet = Slot ( UnifSet ‘ ndx )
4 unifndxnbasendx ( UnifSet ‘ ndx ) ≠ ( Base ‘ ndx )
5 1 2 3 4 resseqnbas ( 𝐴𝑉𝑈 = ( UnifSet ‘ 𝐻 ) )