Metamath Proof Explorer


Theorem setsidel

Description: The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021)

Ref Expression
Hypotheses setsidel.s φSV
setsidel.b φBW
setsidel.r R=SsSetAB
Assertion setsidel φABR

Proof

Step Hyp Ref Expression
1 setsidel.s φSV
2 setsidel.b φBW
3 setsidel.r R=SsSetAB
4 opex ABV
5 4 snid ABAB
6 elun2 ABABABSVAAB
7 5 6 mp1i φABSVAAB
8 setsval SVBWSsSetAB=SVAAB
9 1 2 8 syl2anc φSsSetAB=SVAAB
10 3 9 eqtrid φR=SVAAB
11 7 10 eleqtrrd φABR