This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem inpr0

Description: Rewrite an empty intersection with a pair. (Contributed by Thierry Arnoux, 20-Nov-2023)

Ref Expression
Assertion inpr0 
|- ( ( A i^i { B , C } ) = (/) <-> ( -. B e. A /\ -. C e. A ) )

Proof

Step Hyp Ref Expression
1 r19.26 
 |-  ( A. x e. A ( x =/= B /\ x =/= C ) <-> ( A. x e. A x =/= B /\ A. x e. A x =/= C ) )
2 nelpr 
 |-  ( x e. _V -> ( -. x e. { B , C } <-> ( x =/= B /\ x =/= C ) ) )
3 2 elv 
 |-  ( -. x e. { B , C } <-> ( x =/= B /\ x =/= C ) )
4 3 imbi2i 
 |-  ( ( x e. A -> -. x e. { B , C } ) <-> ( x e. A -> ( x =/= B /\ x =/= C ) ) )
5 4 albii 
 |-  ( A. x ( x e. A -> -. x e. { B , C } ) <-> A. x ( x e. A -> ( x =/= B /\ x =/= C ) ) )
6 disj1 
 |-  ( ( A i^i { B , C } ) = (/) <-> A. x ( x e. A -> -. x e. { B , C } ) )
7 df-ral 
 |-  ( A. x e. A ( x =/= B /\ x =/= C ) <-> A. x ( x e. A -> ( x =/= B /\ x =/= C ) ) )
8 5 6 7 3bitr4i 
 |-  ( ( A i^i { B , C } ) = (/) <-> A. x e. A ( x =/= B /\ x =/= C ) )
9 nelb 
 |-  ( -. B e. A <-> A. x e. A x =/= B )
10 nelb 
 |-  ( -. C e. A <-> A. x e. A x =/= C )
11 9 10 anbi12i 
 |-  ( ( -. B e. A /\ -. C e. A ) <-> ( A. x e. A x =/= B /\ A. x e. A x =/= C ) )
12 1 8 11 3bitr4i 
 |-  ( ( A i^i { B , C } ) = (/) <-> ( -. B e. A /\ -. C e. A ) )