Metamath Proof Explorer

Theorem elioo2

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

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

Proof

Step Hyp Ref Expression
1 iooval2 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) = { x e. RR | ( A < x /\ x < B ) } )
2 1 eleq2d 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,) B ) <-> C e. { x e. RR | ( A < x /\ x < B ) } ) )
3 breq2 
 |-  ( x = C -> ( A < x <-> A < C ) )
4 breq1 
 |-  ( x = C -> ( x < B <-> C < B ) )
5 3 4 anbi12d 
 |-  ( x = C -> ( ( A < x /\ x < B ) <-> ( A < C /\ C < B ) ) )
6 5 elrab 
 |-  ( C e. { x e. RR | ( A < x /\ x < B ) } <-> ( C e. RR /\ ( A < C /\ C < B ) ) )
7 3anass 
 |-  ( ( C e. RR /\ A < C /\ C < B ) <-> ( C e. RR /\ ( A < C /\ C < B ) ) )
8 6 7 bitr4i 
 |-  ( C e. { x e. RR | ( A < x /\ x < B ) } <-> ( C e. RR /\ A < C /\ C < B ) )
9 2 8 bitrdi 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,) B ) <-> ( C e. RR /\ A < C /\ C < B ) ) )