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

Metamath Proof Explorer

Theorem snres0

Description: Condition for restriction of a singleton to be empty. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypothesis snres0.1 
|- B e. _V
Assertion snres0 
|- ( ( { <. A , B >. } |` C ) = (/) <-> -. A e. C )

Proof

Step Hyp Ref Expression
1 snres0.1 
 |-  B e. _V
2 relres 
 |-  Rel ( { <. A , B >. } |` C )
3 reldm0 
 |-  ( Rel ( { <. A , B >. } |` C ) -> ( ( { <. A , B >. } |` C ) = (/) <-> dom ( { <. A , B >. } |` C ) = (/) ) )
4 2 3 ax-mp 
 |-  ( ( { <. A , B >. } |` C ) = (/) <-> dom ( { <. A , B >. } |` C ) = (/) )
5 dmres 
 |-  dom ( { <. A , B >. } |` C ) = ( C i^i dom { <. A , B >. } )
6 1 dmsnop 
 |-  dom { <. A , B >. } = { A }
7 6 ineq2i 
 |-  ( C i^i dom { <. A , B >. } ) = ( C i^i { A } )
8 5 7 eqtri 
 |-  dom ( { <. A , B >. } |` C ) = ( C i^i { A } )
9 8 eqeq1i 
 |-  ( dom ( { <. A , B >. } |` C ) = (/) <-> ( C i^i { A } ) = (/) )
10 disjsn 
 |-  ( ( C i^i { A } ) = (/) <-> -. A e. C )
11 4 9 10 3bitri 
 |-  ( ( { <. A , B >. } |` C ) = (/) <-> -. A e. C )