Theorem elioo2 13448

Description: Membership in an open interval of extended reals. (Contributed by NM, 6-Feb-2007.)

Assertion

Ref	Expression
elioo2	⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))

Proof of Theorem elioo2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iooval2 13440	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)})
2	1	eleq2d 2830	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ 𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}))
3		breq2 5170	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝐴 < 𝑥 ↔ 𝐴 < 𝐶))
4		breq1 5169	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝑥 < 𝐵 ↔ 𝐶 < 𝐵))
5	3, 4	anbi12d 631	. . . 4 ⊢ (𝑥 = 𝐶 → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
6	5	elrab 3708	. . 3 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
7		3anass 1095	. . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵) ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
8	6, 7	bitr4i 278	. 2 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))
9	2, 8	bitrdi 287	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  {crab 3443   class class class wbr 5166  (class class class)co 7448  ℝcr 11183  ℝ^*cxr 11323   < clt 11324  (,)cioo 13407

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-pre-lttri 11258  ax-pre-lttrn 11259

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-po 5607  df-so 5608  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-ioo 13411

This theorem is referenced by:  dfrp2  13456  eliooord  13466  elioopnf  13503  elioomnf  13504  difreicc  13544  xov1plusxeqvd  13558  tanhbnd  16209  bl2ioo  24833  xrtgioo  24847  zcld  24854  iccntr  24862  icccmplem2  24864  reconnlem1  24867  reconnlem2  24868  icoopnst  24988  iocopnst  24989  ivthlem3  25507  ovolicc2lem1  25571  ovolicc2lem5  25575  ioombl1lem4  25615  mbfmax  25703  itg2monolem1  25805  itg2monolem3  25807  dvferm1lem  26042  dvferm2lem  26044  dvlip2  26054  dvivthlem1  26067  lhop1lem  26072  lhop  26075  dvcnvrelem1  26076  dvcnvre  26078  itgsubst  26110  sincosq1sgn  26558  sincosq2sgn  26559  sincosq3sgn  26560  sincosq4sgn  26561  coseq00topi  26562  tanabsge  26566  sinq12gt0  26567  sinq12ge0  26568  cosq14gt0  26570  sincos6thpi  26576  sineq0  26584  cos02pilt1  26586  cosq34lt1  26587  cosordlem  26590  cos0pilt1  26592  tanord1  26597  tanord  26598  argregt0  26670  argimgt0  26672  argimlt0  26673  dvloglem  26708  logf1o2  26710  efopnlem2  26717  asinsinlem  26952  acoscos  26954  atanlogsublem  26976  atantan  26984  atanbndlem  26986  atanbnd  26987  atan1  26989  scvxcvx  27047  basellem1  27142  pntibndlem1  27651  pntibnd  27655  pntlemc  27657  padicabvf  27693  padicabvcxp  27694  cnre2csqlem  33856  ivthALT  36301  iooelexlt  37328  itg2gt0cn  37635  iblabsnclem  37643  dvasin  37664  areacirclem1  37668  areacirc  37673  dvrelog3  42022  0nonelalab  42024  cvgdvgrat  44282  radcnvrat  44283  sineq0ALT  44908  ioogtlb  45413  eliood  45416  eliooshift  45424  iooltub  45428  limciccioolb  45542  limcicciooub  45558  cncfioobdlem  45817  ditgeqiooicc  45881  dirkercncflem1  46024  dirkercncflem4  46027  fourierdlem10  46038  fourierdlem32  46060  fourierdlem62  46089  fourierdlem81  46108  fourierdlem82  46109  fourierdlem93  46120  fourierdlem104  46131  fourierdlem111  46138