Metamath Proof Explorer


Theorem setsnidel

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
setsnidel.c φCX
setsnidel.d φDY
setsnidel.s φCDS
setsnidel.n φAC
Assertion setsnidel φCDR

Proof

Step Hyp Ref Expression
1 setsidel.s φSV
2 setsidel.b φBW
3 setsidel.r R=SsSetAB
4 setsnidel.c φCX
5 setsnidel.d φDY
6 setsnidel.s φCDS
7 setsnidel.n φAC
8 4 elexd φCV
9 7 necomd φCA
10 eldifsn CVACVCA
11 8 9 10 sylanbrc φCVA
12 opelres DYCDSVACVACDS
13 5 12 syl φCDSVACVACDS
14 11 6 13 mpbir2and φCDSVA
15 elun1 CDSVACDSVAAB
16 14 15 syl φCDSVAAB
17 setsval SVBWSsSetAB=SVAAB
18 1 2 17 syl2anc φSsSetAB=SVAAB
19 3 18 eqtrid φR=SVAAB
20 16 19 eleqtrrd φCDR