Theorem elrest 17347

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 17346	. . 3 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐽 ↾t 𝐵) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)))
2	1	eleq2d 2822	. 2 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ 𝐴 ∈ ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵))))
3		eqid 2736	. . 3 ⊢ (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) = (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵))
4		vex 3444	. . . 4 ⊢ 𝑥 ∈ V
5	4	inex1 5262	. . 3 ⊢ (𝑥 ∩ 𝐵) ∈ V
6	3, 5	elrnmpti 5911	. 2 ⊢ (𝐴 ∈ ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵))
7	2, 6	bitrdi 287	1 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∃wrex 3060   ∩ cin 3900   ↦ cmpt 5179  ran crn 5625  (class class class)co 7358   ↾_t crest 17340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-rest 17342

This theorem is referenced by:  elrestr  17348  restsspw  17351  firest  17352  restbas  23102  restsn  23114  restcld  23116  restopnb  23119  ssrest  23120  neitr  23124  restntr  23126  cnrest2  23230  cnpresti  23232  cnprest  23233  cnprest2  23234  lmss  23242  cmpsublem  23343  cmpsub  23344  connsuba  23364  1stcrest  23397  subislly  23425  cldllycmp  23439  txrest  23575  trfbas2  23787  trfbas  23788  trfil2  23831  flimrest  23927  fclsrest  23968  cnextcn  24011  tsmssubm  24087  trust  24173  restutop  24181  restutopopn  24182  trcfilu  24237  metrest  24468  xrtgioo  24751  xrge0tsms  24779  icoopnst  24892  iocopnst  24893  subopnmbl  25561  mbfimaopn2  25614  xrlimcnp  26934  xrge0tsmsd  33155  rspectopn  34024  bj-restsn  37283  bj-rest10  37289  bj-restn0  37291  bj-restpw  37293  bj-rest0  37294  bj-restb  37295  bj-restuni  37298  bj-restreg  37300  ptrest  37816  poimirlem29  37846  elrestd  45348  restuni3  45358  restsubel  45393  icccncfext  46127  subsaliuncl  46598  subsalsal  46599  salrestss  46601  sssmf  46978  incsmf  46982  decsmf  47007  smflimlem6  47016  smfco  47042  smfpimcc  47048