Theorem elioo2 9882

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 9876	. . 3 |- ( ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) = { x e. RR | ( A < x /\ x < B ) } )
2	1	eleq2d 2241	. 2 |- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,) B ) <-> C e. { x e. RR | ( A < x /\ x < B ) } ) )
3		breq2 3994	. . . . 5 |- ( x = C -> ( A < x <-> A < C ) )
4		breq1 3993	. . . . 5 |- ( x = C -> ( x < B <-> C < B ) )
5	3, 4	anbi12d 471	. . . 4 |- ( x = C -> ( ( A < x /\ x < B ) <-> ( A < C /\ C < B ) ) )
6	5	elrab 2887	. . 3 |- ( C e. { x e. RR | ( A < x /\ x < B ) } <-> ( C e. RR /\ ( A < C /\ C < B ) ) )
7		3anass 978	. . 3 |- ( ( C e. RR /\ A < C /\ C < B ) <-> ( C e. RR /\ ( A < C /\ C < B ) ) )
8	6, 7	bitr4i 186	. 2 |- ( C e. { x e. RR | ( A < x /\ x < B ) } <-> ( C e. RR /\ A < C /\ C < B ) )
9	2, 8	bitrdi 195	1 |- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,) B ) <-> ( C e. RR /\ A < C /\ C < B ) ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   /\ w3a 974   = wceq 1349   e. wcel 2142   {crab 2453   class class class wbr 3990  (class class class)co 5857   RRcr 7777   RR*cxr 7957   < clt 7958   (,)cioo 9849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 610  ax-in2 611  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-13 2144  ax-14 2145  ax-ext 2153  ax-sep 4108  ax-pow 4161  ax-pr 4195  ax-un 4419  ax-setind 4522  ax-cnex 7869  ax-resscn 7870  ax-pre-ltirr 7890  ax-pre-ltwlin 7891  ax-pre-lttrn 7892

This theorem depends on definitions:  df-bi 116  df-3or 975  df-3an 976  df-tru 1352  df-fal 1355  df-nf 1455  df-sb 1757  df-eu 2023  df-mo 2024  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ne 2342  df-nel 2437  df-ral 2454  df-rex 2455  df-rab 2458  df-v 2733  df-sbc 2957  df-dif 3124  df-un 3126  df-in 3128  df-ss 3135  df-pw 3569  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-br 3991  df-opab 4052  df-id 4279  df-po 4282  df-iso 4283  df-xp 4618  df-rel 4619  df-cnv 4620  df-co 4621  df-dm 4622  df-iota 5162  df-fun 5202  df-fv 5208  df-ov 5860  df-oprab 5861  df-mpo 5862  df-pnf 7960  df-mnf 7961  df-xr 7962  df-ltxr 7963  df-le 7964  df-ioo 9853

This theorem is referenced by:  eliooord  9889  elioopnf  9928  elioomnf  9929  dfrp2  10224  bl2ioo  13421  dedekindicc  13490  reeff1oleme  13572  reeff1o  13573  sin0pilem2  13582  pilem3  13583  sincosq1sgn  13626  sincosq2sgn  13627  sincosq3sgn  13628  sincosq4sgn  13629  sinq12gt0  13630  cosq14gt0  13632  cosq23lt0  13633  coseq0q4123  13634  coseq00topi  13635  coseq0negpitopi  13636  sincos6thpi  13642  cosordlem  13649  cos02pilt1  13651  cos0pilt1  13652  ioocosf1o  13654  iooref1o  14151  taupi  14187