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 ) ) )