Theorem elioo2 11666

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 11658	. . 3 |- ( ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) = { x e. RR | ( A < x /\ x < B ) } )
2	1	eleq2d 2514	. 2 |- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,) B ) <-> C e. { x e. RR | ( A < x /\ x < B ) } ) )
3		breq2 4377	. . . . 5 |- ( x = C -> ( A < x <-> A < C ) )
4		breq1 4376	. . . . 5 |- ( x = C -> ( x < B <-> C < B ) )
5	3, 4	anbi12d 722	. . . 4 |- ( x = C -> ( ( A < x /\ x < B ) <-> ( A < C /\ C < B ) ) )
6	5	elrab 3163	. . 3 |- ( C e. { x e. RR | ( A < x /\ x < B ) } <-> ( C e. RR /\ ( A < C /\ C < B ) ) )
7		3anass 990	. . 3 |- ( ( C e. RR /\ A < C /\ C < B ) <-> ( C e. RR /\ ( A < C /\ C < B ) ) )
8	6, 7	bitr4i 260	. 2 |- ( C e. { x e. RR | ( A < x /\ x < B ) } <-> ( C e. RR /\ A < C /\ C < B ) )
9	2, 8	syl6bb 269	1 |- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,) B ) <-> ( C e. RR /\ A < C /\ C < B ) ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   /\ w3a 986   = wceq 1447   e. wcel 1890   {crab 2740   class class class wbr 4373  (class class class)co 6275   RRcr 9524   RR*cxr 9660   < clt 9661   (,)cioo 11624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570  ax-cnex 9581  ax-resscn 9582  ax-pre-lttri 9599  ax-pre-lttrn 9600

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-op 3942  df-uni 4168  df-iun 4249  df-br 4374  df-opab 4433  df-mpt 4434  df-id 4726  df-po 4732  df-so 4733  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-f1 5565  df-fo 5566  df-f1o 5567  df-fv 5568  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-1st 6780  df-2nd 6781  df-er 7349  df-en 7556  df-dom 7557  df-sdom 7558  df-pnf 9663  df-mnf 9664  df-xr 9665  df-ltxr 9666  df-le 9667  df-ioo 11628

This theorem is referenced by:  eliooord  11683  elioopnf  11717  elioomnf  11718  difreicc  11754  xov1plusxeqvd  11768  tanhbnd  14225  bl2ioo  21820  xrtgioo  21834  zcld  21841  iccntr  21849  icccmplem2  21851  reconnlem1  21854  reconnlem2  21855  icoopnst  21977  iocopnst  21978  ivthlem3  22414  ovolicc2lem1  22480  ovolicc2lem5  22485  ioombl1lem4  22525  mbfmax  22616  itg2monolem1  22719  itg2monolem3  22721  dvferm1lem  22947  dvferm2lem  22949  dvlip2  22958  dvivthlem1  22971  lhop1lem  22976  lhop  22979  dvcnvrelem1  22980  dvcnvre  22982  itgsubst  23012  sincosq1sgn  23464  sincosq2sgn  23465  sincosq3sgn  23466  sincosq4sgn  23467  coseq00topi  23468  tanabsge  23472  sinq12gt0  23473  sinq12ge0  23474  cosq14gt0  23476  sincos6thpi  23481  sineq0  23487  cosordlem  23491  tanord1  23497  tanord  23498  argregt0  23570  argimgt0  23572  argimlt0  23573  dvloglem  23604  logf1o2  23606  efopnlem2  23613  asinsinlem  23828  acoscos  23830  atanlogsublem  23852  atantan  23860  atanbndlem  23862  atanbnd  23863  atan1  23865  scvxcvx  23922  basellem1  24018  pntibndlem1  24438  pntibnd  24442  pntlemc  24444  padicabvf  24480  padicabvcxp  24481  dfrp2  28359  cnre2csqlem  28722  ivthALT  30996  iooelexlt  31766  dvtanlemOLD  31992  itg2gt0cn  31998  iblabsnclem  32006  dvasin  32029  areacirclem1  32033  areacirc  32038  cvgdvgrat  36662  radcnvrat  36663  sineq0ALT  37330  ioogtlb  37632  eliood  37635  eliooshift  37644  iooltub  37650  limciccioolb  37742  limcicciooub  37758  cncfioobdlem  37815  ditgeqiooicc  37878  dirkercncflem1  38021  dirkercncflem4  38024  fourierdlem10  38035  fourierdlem32  38058  fourierdlem62  38088  fourierdlem81  38107  fourierdlem82  38108  fourierdlem93  38119  fourierdlem104  38130  fourierdlem111  38137