Theorem elrest 17372

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 17371	. . 3 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐽 ↾t 𝐵) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)))
2	1	eleq2d 2819	. 2 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ 𝐴 ∈ ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵))))
3		eqid 2732	. . 3 ⊢ (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) = (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵))
4		vex 3478	. . . 4 ⊢ 𝑥 ∈ V
5	4	inex1 5317	. . 3 ⊢ (𝑥 ∩ 𝐵) ∈ V
6	3, 5	elrnmpti 5959	. 2 ⊢ (𝐴 ∈ ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵))
7	2, 6	bitrdi 286	1 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∃wrex 3070   ∩ cin 3947   ↦ cmpt 5231  ran crn 5677  (class class class)co 7408   ↾_t crest 17365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7724

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-rest 17367

This theorem is referenced by:  elrestr  17373  restsspw  17376  firest  17377  restbas  22661  restsn  22673  restcld  22675  restopnb  22678  ssrest  22679  neitr  22683  restntr  22685  cnrest2  22789  cnpresti  22791  cnprest  22792  cnprest2  22793  lmss  22801  cmpsublem  22902  cmpsub  22903  connsuba  22923  1stcrest  22956  subislly  22984  cldllycmp  22998  txrest  23134  trfbas2  23346  trfbas  23347  trfil2  23390  flimrest  23486  fclsrest  23527  cnextcn  23570  tsmssubm  23646  trust  23733  restutop  23741  restutopopn  23742  trcfilu  23798  metrest  24032  xrtgioo  24321  xrge0tsms  24349  icoopnst  24454  iocopnst  24455  subopnmbl  25120  mbfimaopn2  25173  xrlimcnp  26470  xrge0tsmsd  32204  rspectopn  32842  bj-restsn  35958  bj-rest10  35964  bj-restn0  35966  bj-restpw  35968  bj-rest0  35969  bj-restb  35970  bj-restuni  35973  bj-restreg  35975  ptrest  36482  poimirlem29  36512  elrestd  43787  restuni3  43797  restsubel  43837  icccncfext  44593  subsaliuncl  45064  subsalsal  45065  salrestss  45067  sssmf  45444  incsmf  45448  decsmf  45473  smflimlem6  45482  smfco  45508  smfpimcc  45514