Theorem elrest 17473

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 17472	. . 3 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐽 ↾t 𝐵) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)))
2	1	eleq2d 2824	. 2 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ 𝐴 ∈ ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵))))
3		eqid 2734	. . 3 ⊢ (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) = (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵))
4		vex 3481	. . . 4 ⊢ 𝑥 ∈ V
5	4	inex1 5322	. . 3 ⊢ (𝑥 ∩ 𝐵) ∈ V
6	3, 5	elrnmpti 5975	. 2 ⊢ (𝐴 ∈ ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵))
7	2, 6	bitrdi 287	1 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536   ∈ wcel 2105  ∃wrex 3067   ∩ cin 3961   ↦ cmpt 5230  ran crn 5689  (class class class)co 7430   ↾_t crest 17466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-rest 17468

This theorem is referenced by:  elrestr  17474  restsspw  17477  firest  17478  restbas  23181  restsn  23193  restcld  23195  restopnb  23198  ssrest  23199  neitr  23203  restntr  23205  cnrest2  23309  cnpresti  23311  cnprest  23312  cnprest2  23313  lmss  23321  cmpsublem  23422  cmpsub  23423  connsuba  23443  1stcrest  23476  subislly  23504  cldllycmp  23518  txrest  23654  trfbas2  23866  trfbas  23867  trfil2  23910  flimrest  24006  fclsrest  24047  cnextcn  24090  tsmssubm  24166  trust  24253  restutop  24261  restutopopn  24262  trcfilu  24318  metrest  24552  xrtgioo  24841  xrge0tsms  24869  icoopnst  24982  iocopnst  24983  subopnmbl  25652  mbfimaopn2  25705  xrlimcnp  27025  xrge0tsmsd  33047  rspectopn  33827  bj-restsn  37064  bj-rest10  37070  bj-restn0  37072  bj-restpw  37074  bj-rest0  37075  bj-restb  37076  bj-restuni  37079  bj-restreg  37081  ptrest  37605  poimirlem29  37635  elrestd  45047  restuni3  45057  restsubel  45095  icccncfext  45842  subsaliuncl  46313  subsalsal  46314  salrestss  46316  sssmf  46693  incsmf  46697  decsmf  46722  smflimlem6  46731  smfco  46757  smfpimcc  46763