Theorem elrest 16535

Description: The predicate "is an open set of a subspace topology". (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)

Assertion

Ref	Expression
elrest	⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵)))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐽

Allowed substitution hints:   𝑉(𝑥)   𝑊(𝑥)

Proof of Theorem elrest

Step	Hyp	Ref	Expression
1		restval 16534	. . 3 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐽 ↾t 𝐵) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)))
2	1	eleq2d 2868	. 2 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ 𝐴 ∈ ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵))))
3		eqid 2795	. . 3 ⊢ (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) = (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵))
4		vex 3440	. . . 4 ⊢ 𝑥 ∈ V
5	4	inex1 5117	. . 3 ⊢ (𝑥 ∩ 𝐵) ∈ V
6	3, 5	elrnmpti 5719	. 2 ⊢ (𝐴 ∈ ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵))
7	2, 6	syl6bb 288	1 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1522   ∈ wcel 2081  ∃wrex 3106   ∩ cin 3862   ↦ cmpt 5045  ran crn 5449  (class class class)co 7021   ↾_t crest 16528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5086  ax-sep 5099  ax-nul 5106  ax-pr 5226  ax-un 7324

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-reu 3112  df-rab 3114  df-v 3439  df-sbc 3710  df-csb 3816  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-iun 4831  df-br 4967  df-opab 5029  df-mpt 5046  df-id 5353  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-f1 6235  df-fo 6236  df-f1o 6237  df-fv 6238  df-ov 7024  df-oprab 7025  df-mpo 7026  df-rest 16530

This theorem is referenced by:  elrestr  16536  restsspw  16539  firest  16540  restbas  21455  restsn  21467  restcld  21469  restopnb  21472  ssrest  21473  neitr  21477  restntr  21479  cnrest2  21583  cnpresti  21585  cnprest  21586  cnprest2  21587  lmss  21595  cmpsublem  21696  cmpsub  21697  connsuba  21717  1stcrest  21750  subislly  21778  cldllycmp  21792  txrest  21928  trfbas2  22140  trfbas  22141  trfil2  22184  flimrest  22280  fclsrest  22321  cnextcn  22364  tsmssubm  22439  trust  22526  restutop  22534  restutopopn  22535  trcfilu  22591  metrest  22822  xrtgioo  23102  xrge0tsms  23130  icoopnst  23231  iocopnst  23232  subopnmbl  23893  mbfimaopn2  23946  xrlimcnp  25233  xrge0tsmsd  30508  bj-restsn  33997  bj-rest10  34003  bj-restn0  34005  bj-restpw  34007  bj-rest0  34008  bj-restb  34009  bj-restuni  34012  bj-restreg  34014  ptrest  34447  poimirlem29  34477  elrestd  40939  restuni3  40949  icccncfext  41737  subsaliuncl  42209  subsalsal  42210  sssmf  42583  incsmf  42587  decsmf  42611  smflimlem6  42620  smfco  42645  smfpimcc  42650