Metamath Proof Explorer

Theorem indifdirOLD

Description: Obsolete version of indifdir as of 14-Aug-2024. (Contributed by Scott Fenton, 14-Apr-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion indifdirOLD 
|- ( ( A \ B ) i^i C ) = ( ( A i^i C ) \ ( B i^i C ) )

Proof

Step Hyp Ref Expression
1 pm3.24 
 |-  -. ( x e. C /\ -. x e. C )
2 1 intnan 
 |-  -. ( x e. A /\ ( x e. C /\ -. x e. C ) )
3 anass 
 |-  ( ( ( x e. A /\ x e. C ) /\ -. x e. C ) <-> ( x e. A /\ ( x e. C /\ -. x e. C ) ) )
4 2 3 mtbir 
 |-  -. ( ( x e. A /\ x e. C ) /\ -. x e. C )
5 4 biorfi 
 |-  ( ( ( x e. A /\ x e. C ) /\ -. x e. B ) <-> ( ( ( x e. A /\ x e. C ) /\ -. x e. B ) \/ ( ( x e. A /\ x e. C ) /\ -. x e. C ) ) )
6 an32 
 |-  ( ( ( x e. A /\ -. x e. B ) /\ x e. C ) <-> ( ( x e. A /\ x e. C ) /\ -. x e. B ) )
7 andi 
 |-  ( ( ( x e. A /\ x e. C ) /\ ( -. x e. B \/ -. x e. C ) ) <-> ( ( ( x e. A /\ x e. C ) /\ -. x e. B ) \/ ( ( x e. A /\ x e. C ) /\ -. x e. C ) ) )
8 5 6 7 3bitr4i 
 |-  ( ( ( x e. A /\ -. x e. B ) /\ x e. C ) <-> ( ( x e. A /\ x e. C ) /\ ( -. x e. B \/ -. x e. C ) ) )
9 ianor 
 |-  ( -. ( x e. B /\ x e. C ) <-> ( -. x e. B \/ -. x e. C ) )
10 9 anbi2i 
 |-  ( ( ( x e. A /\ x e. C ) /\ -. ( x e. B /\ x e. C ) ) <-> ( ( x e. A /\ x e. C ) /\ ( -. x e. B \/ -. x e. C ) ) )
11 8 10 bitr4i 
 |-  ( ( ( x e. A /\ -. x e. B ) /\ x e. C ) <-> ( ( x e. A /\ x e. C ) /\ -. ( x e. B /\ x e. C ) ) )
12 elin 
 |-  ( x e. ( ( A \ B ) i^i C ) <-> ( x e. ( A \ B ) /\ x e. C ) )
13 eldif 
 |-  ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
14 13 anbi1i 
 |-  ( ( x e. ( A \ B ) /\ x e. C ) <-> ( ( x e. A /\ -. x e. B ) /\ x e. C ) )
15 12 14 bitri 
 |-  ( x e. ( ( A \ B ) i^i C ) <-> ( ( x e. A /\ -. x e. B ) /\ x e. C ) )
16 eldif 
 |-  ( x e. ( ( A i^i C ) \ ( B i^i C ) ) <-> ( x e. ( A i^i C ) /\ -. x e. ( B i^i C ) ) )
17 elin 
 |-  ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
18 elin 
 |-  ( x e. ( B i^i C ) <-> ( x e. B /\ x e. C ) )
19 18 notbii 
 |-  ( -. x e. ( B i^i C ) <-> -. ( x e. B /\ x e. C ) )
20 17 19 anbi12i 
 |-  ( ( x e. ( A i^i C ) /\ -. x e. ( B i^i C ) ) <-> ( ( x e. A /\ x e. C ) /\ -. ( x e. B /\ x e. C ) ) )
21 16 20 bitri 
 |-  ( x e. ( ( A i^i C ) \ ( B i^i C ) ) <-> ( ( x e. A /\ x e. C ) /\ -. ( x e. B /\ x e. C ) ) )
22 11 15 21 3bitr4i 
 |-  ( x e. ( ( A \ B ) i^i C ) <-> x e. ( ( A i^i C ) \ ( B i^i C ) ) )
23 22 eqriv 
 |-  ( ( A \ B ) i^i C ) = ( ( A i^i C ) \ ( B i^i C ) )