Theorem elbl 24366

Description: Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)

Assertion

Ref	Expression
elbl	⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴 ∈ 𝑋 ∧ (𝑃𝐷𝐴) < 𝑅)))

Proof of Theorem elbl

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		blval 24364	. . 3 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) = {𝑥 ∈ 𝑋 ∣ (𝑃𝐷𝑥) < 𝑅})
2	1	eleq2d 2823	. 2 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ 𝐴 ∈ {𝑥 ∈ 𝑋 ∣ (𝑃𝐷𝑥) < 𝑅}))
3		oveq2 7369	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑃𝐷𝑥) = (𝑃𝐷𝐴))
4	3	breq1d 5096	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑃𝐷𝑥) < 𝑅 ↔ (𝑃𝐷𝐴) < 𝑅))
5	4	elrab 3635	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑋 ∣ (𝑃𝐷𝑥) < 𝑅} ↔ (𝐴 ∈ 𝑋 ∧ (𝑃𝐷𝐴) < 𝑅))
6	2, 5	bitrdi 287	1 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴 ∈ 𝑋 ∧ (𝑃𝐷𝐴) < 𝑅)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  {crab 3390   class class class wbr 5086  ‘cfv 6493  (class class class)co 7361  ℝ^*cxr 11172   < clt 11173  ∞Metcxmet 21332  ballcbl 21334

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-resscn 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7364  df-oprab 7365  df-mpo 7366  df-1st 7936  df-2nd 7937  df-map 8769  df-xr 11177  df-psmet 21339  df-xmet 21340  df-bl 21342

This theorem is referenced by:  elbl2  24368  xblpnf  24374  bldisj  24376  blgt0  24377  xblss2  24380  blhalf  24383  xblcntr  24389  xbln0  24392  blin  24399  blss  24403  blres  24409  imasf1obl  24466  prdsbl  24469  blcls  24484  metcnp  24519  dscopn  24551  cnbl0  24751  bl2ioo  24770  blcvx  24776  xrsmopn  24791  recld2  24793  cnheibor  24935  nmhmcn  25100  lmmbr2  25239  iscau2  25257  dvlip2  25975  psercn  26407  abelth  26422  logtayl  26640  logtayl2  26642  poimirlem29  37987  heicant  37993  iooabslt  45950  limcrecl  46080  islpcn  46088  qndenserrnbllem  46743