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

Metamath Proof Explorer

Theorem difrab2

Description: Difference of two restricted class abstractions. Compare with difrab . (Contributed by Thierry Arnoux, 3-Jan-2022)

Ref Expression
Assertion difrab2 
|- ( { x e. A | ph } \ { x e. B | ph } ) = { x e. ( A \ B ) | ph }

Proof

Step Hyp Ref Expression
1 nfrab1 
 |-  F/_ x { x e. A | ph }
2 nfrab1 
 |-  F/_ x { x e. B | ph }
3 1 2 nfdif 
 |-  F/_ x ( { x e. A | ph } \ { x e. B | ph } )
4 nfrab1 
 |-  F/_ x { x e. ( A \ B ) | ph }
5 eldif 
 |-  ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
6 5 anbi1i 
 |-  ( ( x e. ( A \ B ) /\ ph ) <-> ( ( x e. A /\ -. x e. B ) /\ ph ) )
7 andi 
 |-  ( ( ph /\ ( -. x e. B \/ -. ph ) ) <-> ( ( ph /\ -. x e. B ) \/ ( ph /\ -. ph ) ) )
8 pm3.24 
 |-  -. ( ph /\ -. ph )
9 8 biorfri 
 |-  ( ( ph /\ -. x e. B ) <-> ( ( ph /\ -. x e. B ) \/ ( ph /\ -. ph ) ) )
10 ancom 
 |-  ( ( ph /\ -. x e. B ) <-> ( -. x e. B /\ ph ) )
11 7 9 10 3bitr2i 
 |-  ( ( ph /\ ( -. x e. B \/ -. ph ) ) <-> ( -. x e. B /\ ph ) )
12 11 anbi2i 
 |-  ( ( x e. A /\ ( ph /\ ( -. x e. B \/ -. ph ) ) ) <-> ( x e. A /\ ( -. x e. B /\ ph ) ) )
13 anass 
 |-  ( ( ( x e. A /\ ph ) /\ ( -. x e. B \/ -. ph ) ) <-> ( x e. A /\ ( ph /\ ( -. x e. B \/ -. ph ) ) ) )
14 anass 
 |-  ( ( ( x e. A /\ -. x e. B ) /\ ph ) <-> ( x e. A /\ ( -. x e. B /\ ph ) ) )
15 12 13 14 3bitr4i 
 |-  ( ( ( x e. A /\ ph ) /\ ( -. x e. B \/ -. ph ) ) <-> ( ( x e. A /\ -. x e. B ) /\ ph ) )
16 6 15 bitr4i 
 |-  ( ( x e. ( A \ B ) /\ ph ) <-> ( ( x e. A /\ ph ) /\ ( -. x e. B \/ -. ph ) ) )
17 rabid 
 |-  ( x e. { x e. ( A \ B ) | ph } <-> ( x e. ( A \ B ) /\ ph ) )
18 eldif 
 |-  ( x e. ( { x e. A | ph } \ { x e. B | ph } ) <-> ( x e. { x e. A | ph } /\ -. x e. { x e. B | ph } ) )
19 rabid 
 |-  ( x e. { x e. A | ph } <-> ( x e. A /\ ph ) )
20 ianor 
 |-  ( -. ( x e. B /\ ph ) <-> ( -. x e. B \/ -. ph ) )
21 rabid 
 |-  ( x e. { x e. B | ph } <-> ( x e. B /\ ph ) )
22 20 21 xchnxbir 
 |-  ( -. x e. { x e. B | ph } <-> ( -. x e. B \/ -. ph ) )
23 19 22 anbi12i 
 |-  ( ( x e. { x e. A | ph } /\ -. x e. { x e. B | ph } ) <-> ( ( x e. A /\ ph ) /\ ( -. x e. B \/ -. ph ) ) )
24 18 23 bitri 
 |-  ( x e. ( { x e. A | ph } \ { x e. B | ph } ) <-> ( ( x e. A /\ ph ) /\ ( -. x e. B \/ -. ph ) ) )
25 16 17 24 3bitr4ri 
 |-  ( x e. ( { x e. A | ph } \ { x e. B | ph } ) <-> x e. { x e. ( A \ B ) | ph } )
26 3 4 25 eqri 
 |-  ( { x e. A | ph } \ { x e. B | ph } ) = { x e. ( A \ B ) | ph }