Theorem elrestr 16775

Description: Sufficient condition for being an open set in a subspace. (Contributed by Jeff Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)

Assertion

Ref	Expression
elrestr	⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐴 ∈ 𝐽) → (𝐴 ∩ 𝑆) ∈ (𝐽 ↾t 𝑆))

Proof of Theorem elrestr

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2759	. . . 4 ⊢ (𝐴 ∩ 𝑆) = (𝐴 ∩ 𝑆)
2		ineq1 4112	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝑆) = (𝐴 ∩ 𝑆))
3	2	rspceeqv 3559	. . . 4 ⊢ ((𝐴 ∈ 𝐽 ∧ (𝐴 ∩ 𝑆) = (𝐴 ∩ 𝑆)) → ∃𝑥 ∈ 𝐽 (𝐴 ∩ 𝑆) = (𝑥 ∩ 𝑆))
4	1, 3	mpan2 690	. . 3 ⊢ (𝐴 ∈ 𝐽 → ∃𝑥 ∈ 𝐽 (𝐴 ∩ 𝑆) = (𝑥 ∩ 𝑆))
5		elrest 16774	. . 3 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → ((𝐴 ∩ 𝑆) ∈ (𝐽 ↾t 𝑆) ↔ ∃𝑥 ∈ 𝐽 (𝐴 ∩ 𝑆) = (𝑥 ∩ 𝑆)))
6	4, 5	syl5ibr 249	. 2 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐴 ∈ 𝐽 → (𝐴 ∩ 𝑆) ∈ (𝐽 ↾t 𝑆)))
7	6	3impia 1115	1 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐴 ∈ 𝐽) → (𝐴 ∩ 𝑆) ∈ (𝐽 ↾t 𝑆))

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112  ∃wrex 3072   ∩ cin 3860  (class class class)co 7157   ↾_t crest 16767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5161  ax-sep 5174  ax-nul 5181  ax-pr 5303  ax-un 7466

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-nul 4229  df-if 4425  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4803  df-iun 4889  df-br 5038  df-opab 5100  df-mpt 5118  df-id 5435  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-ov 7160  df-oprab 7161  df-mpo 7162  df-rest 16769

This theorem is referenced by:  firest  16779  restbas  21873  tgrest  21874  resttopon  21876  restcld  21887  restfpw  21894  neitr  21895  restntr  21897  ordtrest  21917  cnrest  22000  lmss  22013  connsubclo  22139  restnlly  22197  islly2  22199  cldllycmp  22210  lly1stc  22211  kgenss  22258  xkococnlem  22374  xkoinjcn  22402  qtoprest  22432  trfbas2  22558  trfil1  22601  trfil2  22602  fgtr  22605  trfg  22606  uzrest  22612  trufil  22625  flimrest  22698  cnextcn  22782  trust  22945  restutop  22953  trcfilu  23010  cfiluweak  23011  xrsmopn  23528  zdis  23532  xrge0tsms  23550  cnheibor  23671  cfilres  24011  lhop2  24729  psercn  25135  xrlimcnp  25668  xrge0tsmsd  30857  ordtrestNEW  31406  pnfneige0  31436  lmxrge0  31437  rrhre  31504  cvmscld  32765  cvmopnlem  32770  cvmliftmolem1  32773  poimirlem30  35403  subspopn  35506  iocopn  42569  icoopn  42574  limcresiooub  42696  limcresioolb  42697  fourierdlem32  43193  fourierdlem33  43194  fourierdlem48  43208  fourierdlem49  43209  i0oii  45665  io1ii  45666  iscnrm3llem2  45696