Metamath Proof Explorer

Theorem ifr0

Description: A class that is founded by the identity relation is null. (Contributed by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion ifr0 
|- ( _I Fr A <-> A = (/) )

Proof

Step Hyp Ref Expression
1 equid 
 |-  x = x
2 vex 
 |-  x e. _V
3 2 ideq 
 |-  ( x _I x <-> x = x )
4 1 3 mpbir 
 |-  x _I x
5 frirr 
 |-  ( ( _I Fr A /\ x e. A ) -> -. x _I x )
6 5 ex 
 |-  ( _I Fr A -> ( x e. A -> -. x _I x ) )
7 4 6 mt2i 
 |-  ( _I Fr A -> -. x e. A )
8 7 eq0rdv 
 |-  ( _I Fr A -> A = (/) )
9 fr0 
 |-  _I Fr (/)
10 freq2 
 |-  ( A = (/) -> ( _I Fr A <-> _I Fr (/) ) )
11 9 10 mpbiri 
 |-  ( A = (/) -> _I Fr A )
12 8 11 impbii 
 |-  ( _I Fr A <-> A = (/) )