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

Metamath Proof Explorer

Theorem isfin4

Description: Definition of a IV-finite set. (Contributed by Stefan O'Rear, 16-May-2015)

Ref Expression
Assertion isfin4 
|- ( A e. V -> ( A e. Fin4 <-> -. E. y ( y C. A /\ y ~~ A ) ) )

Proof

Step Hyp Ref Expression
1 psseq2 
 |-  ( x = A -> ( y C. x <-> y C. A ) )
2 breq2 
 |-  ( x = A -> ( y ~~ x <-> y ~~ A ) )
3 1 2 anbi12d 
 |-  ( x = A -> ( ( y C. x /\ y ~~ x ) <-> ( y C. A /\ y ~~ A ) ) )
4 3 exbidv 
 |-  ( x = A -> ( E. y ( y C. x /\ y ~~ x ) <-> E. y ( y C. A /\ y ~~ A ) ) )
5 4 notbid 
 |-  ( x = A -> ( -. E. y ( y C. x /\ y ~~ x ) <-> -. E. y ( y C. A /\ y ~~ A ) ) )
6 df-fin4 
 |-  Fin4 = { x | -. E. y ( y C. x /\ y ~~ x ) }
7 5 6 elab2g 
 |-  ( A e. V -> ( A e. Fin4 <-> -. E. y ( y C. A /\ y ~~ A ) ) )