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