Theorem elrest 17518

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 17517	. . 3 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐽 ↾t 𝐵) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)))
2	1	eleq2d 2848	. 2 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ 𝐴 ∈ ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵))))
3		eqid 2762	. . 3 ⊢ (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) = (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵))
4		vex 3457	. . . 4 ⊢ 𝑥 ∈ V
5	4	inex1 5284	. . 3 ⊢ (𝑥 ∩ 𝐵) ∈ V
6	3, 5	elrnmpti 5950	. 2 ⊢ (𝐴 ∈ ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵))
7	2, 6	bitrdi 290	1 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∃wrex 3088   ∩ cin 3901   ↦ cmpt 5190  ran crn 5660  (class class class)co 7417   ↾_t crest 17511

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7740

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 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422  df-rest 17513

This theorem is used by:  elrestr  17519  restsspw  17522  firest  17523  restbas  23389  restsn  23401  restcld  23403  restopnb  23406  ssrest  23407  neitr  23411  restntr  23413  cnrest2  23517  cnpresti  23519  cnprest  23520  cnprest2  23521  lmss  23529  cmpsublem  23630  cmpsub  23631  connsuba  23651  1stcrest  23684  subislly  23713  cldllycmp  23727  txrest  23863  trfbas2  24075  trfbas  24076  trfil2  24119  flimrest  24215  fclsrest  24256  cnextcn  24299  tsmssubm  24375  trust  24461  restutop  24469  restutopopn  24470  trcfilu  24525  metrest  24756  xrtgioo  25039  xrge0tsms  25067  icoopnst  25173  iocopnst  25174  subopnmbl  25838  mbfimaopn2  25891  xrlimcnp  27213  xrge0tsmsd  33521  rspectopn  34385  bj-restsn  37840  bj-rest10  37846  bj-restn0  37848  bj-restpw  37850  bj-rest0  37851  bj-restb  37852  bj-restuni  37855  bj-restreg  37857  ptrest  38376  poimirlem29  38406  elrestd  45948  restuni3  45958  restsubel  45993  icccncfext  46723  subsaliuncl  47194  subsalsal  47195  salrestss  47197  sssmf  47574  incsmf  47578  decsmf  47603  smflimlem6  47612  smfco  47638  smfpimcc  47644