Theorem elrest 17627

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 17626	. . 3 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐽 ↾t 𝐵) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)))
2	1	eleq2d 2850	. 2 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ 𝐴 ∈ ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵))))
3		eqid 2763	. . 3 ⊢ (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) = (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵))
4		vex 3458	. . . 4 ⊢ 𝑥 ∈ V
5	4	inex1 5281	. . 3 ⊢ (𝑥 ∩ 𝐵) ∈ V
6	3, 5	elrnmpti 5951	. 2 ⊢ (𝐴 ∈ ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵))
7	2, 6	bitrdi 290	1 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∃wrex 3090   ∩ cin 4092   ↦ cmpt 5189  ran crn 5656  (class class class)co 7443   ↾_t crest 17620

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7775

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-ov 7446  df-oprab 7447  df-mpo 7448  df-rest 17622

This theorem is used by:  elrestr  17628  restsspw  17631  firest  17632  restbas  23506  restsn  23518  restcld  23520  restopnb  23523  ssrest  23524  neitr  23528  restntr  23530  cnrest2  23634  cnpresti  23636  cnprest  23637  cnprest2  23638  lmss  23646  cmpsublem  23747  cmpsub  23748  connsuba  23768  1stcrest  23801  subislly  23830  cldllycmp  23844  txrest  23980  trfbas2  24192  trfbas  24193  trfil2  24236  flimrest  24332  fclsrest  24373  cnextcn  24416  tsmssubm  24492  trust  24578  restutop  24586  restutopopn  24587  trcfilu  24642  metrest  24873  xrtgioo  25156  xrge0tsms  25184  icoopnst  25290  iocopnst  25291  subopnmbl  25955  mbfimaopn2  26008  xrlimcnp  27326  xrge0tsmsd  33704  rspectopn  34569  bj-restsn  38194  bj-rest10  38200  bj-restn0  38202  bj-restpw  38204  bj-rest0  38205  bj-restb  38206  bj-restuni  38209  bj-restreg  38211  ptrest  38729  poimirlem29  38759  elrestd  46328  restuni3  46338  restsubel  46373  icccncfext  47102  subsaliuncl  47573  subsalsal  47574  salrestss  47576  sssmf  47953  incsmf  47957  decsmf  47982  smflimlem6  47991  smfco  48017  smfpimcc  48023