Theorem elioo2 11337

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

Assertion

Ref	Expression
elioo2	|- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,) B ) <-> ( C e. RR /\ A < C /\ C < B ) ) )

Proof of Theorem elioo2

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iooval2 11329	. . 3 |- ( ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) = { x e. RR | ( A < x /\ x < B ) } )
2	1	eleq2d 2508	. 2 |- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,) B ) <-> C e. { x e. RR | ( A < x /\ x < B ) } ) )
3		breq2 4293	. . . . 5 |- ( x = C -> ( A < x <-> A < C ) )
4		breq1 4292	. . . . 5 |- ( x = C -> ( x < B <-> C < B ) )
5	3, 4	anbi12d 705	. . . 4 |- ( x = C -> ( ( A < x /\ x < B ) <-> ( A < C /\ C < B ) ) )
6	5	elrab 3114	. . 3 |- ( C e. { x e. RR | ( A < x /\ x < B ) } <-> ( C e. RR /\ ( A < C /\ C < B ) ) )
7		3anass 964	. . 3 |- ( ( C e. RR /\ A < C /\ C < B ) <-> ( C e. RR /\ ( A < C /\ C < B ) ) )
8	6, 7	bitr4i 252	. 2 |- ( C e. { x e. RR | ( A < x /\ x < B ) } <-> ( C e. RR /\ A < C /\ C < B ) )
9	2, 8	syl6bb 261	1 |- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,) B ) <-> ( C e. RR /\ A < C /\ C < B ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 960   = wceq 1364   e. wcel 1761   {crab 2717   class class class wbr 4289  (class class class)co 6090   RRcr 9277   RR*cxr 9413   < clt 9414   (,)cioo 11296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-cnex 9334  ax-resscn 9335  ax-pre-lttri 9352  ax-pre-lttrn 9353

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-po 4637  df-so 4638  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-1st 6576  df-2nd 6577  df-er 7097  df-en 7307  df-dom 7308  df-sdom 7309  df-pnf 9416  df-mnf 9417  df-xr 9418  df-ltxr 9419  df-le 9420  df-ioo 11300

This theorem is referenced by:  eliooord  11351  elioopnf  11379  elioomnf  11380  difreicc  11413  xov1plusxeqvd  11427  tanhbnd  13441  bl2ioo  20328  xrtgioo  20342  zcld  20349  iccntr  20357  icccmplem2  20359  reconnlem1  20362  reconnlem2  20363  icoopnst  20470  iocopnst  20471  ivthlem3  20896  ovolicc2lem1  20959  ovolicc2lem5  20963  ioombl1lem4  21001  mbfmax  21086  itg2monolem1  21187  itg2monolem3  21189  dvferm1lem  21415  dvferm2lem  21417  dvlip2  21426  dvivthlem1  21439  lhop1lem  21444  lhop  21447  dvcnvrelem1  21448  dvcnvre  21450  itgsubst  21480  sincosq1sgn  21919  sincosq2sgn  21920  sincosq3sgn  21921  sincosq4sgn  21922  coseq00topi  21923  tanabsge  21927  sinq12gt0  21928  sinq12ge0  21929  cosq14gt0  21931  sincos6thpi  21936  sineq0  21942  cosordlem  21946  tanord1  21952  tanord  21953  argregt0  22018  argimgt0  22020  argimlt0  22021  dvloglem  22052  logf1o2  22054  efopnlem2  22061  asinsinlem  22245  acoscos  22247  atanlogsublem  22269  atantan  22277  atanbndlem  22279  atanbnd  22280  atan1  22282  scvxcvx  22338  basellem1  22377  pntibndlem1  22797  pntibnd  22801  pntlemc  22803  padicabvf  22839  padicabvcxp  22840  cnre2csqlem  26276  dvtanlem  28366  itg2gt0cn  28372  iblabsnclem  28380  dvasin  28405  areacirclem1  28409  areacirc  28414  ivthALT  28455  sineq0ALT  31507