Metamath Proof Explorer


Theorem elrestd

Description: A sufficient condition for being an open set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses elrestd.1 φJV
elrestd.2 φBW
elrestd.3 φXJ
elrestd.4 A=XB
Assertion elrestd φAJ𝑡B

Proof

Step Hyp Ref Expression
1 elrestd.1 φJV
2 elrestd.2 φBW
3 elrestd.3 φXJ
4 elrestd.4 A=XB
5 4 a1i φA=XB
6 ineq1 x=XxB=XB
7 6 rspceeqv XJA=XBxJA=xB
8 3 5 7 syl2anc φxJA=xB
9 elrest JVBWAJ𝑡BxJA=xB
10 1 2 9 syl2anc φAJ𝑡BxJA=xB
11 8 10 mpbird φAJ𝑡B