Theorem isfin7

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

	Ref	Expression
Assertion	isfin7	|- ( A e. V -> ( A e. Fin7 <-> -. E. y e. ( On \ _om ) A ~~ y ) )

Proof

Step	Hyp	Ref	Expression
1		breq1	|- ( x = A -> ( x ~~ y <-> A ~~ y ) )
2	1	rexbidv	|- ( x = A -> ( E. y e. ( On \ _om ) x ~~ y <-> E. y e. ( On \ _om ) A ~~ y ) )
3	2	notbid	|- ( x = A -> ( -. E. y e. ( On \ _om ) x ~~ y <-> -. E. y e. ( On \ _om ) A ~~ y ) )
4		df-fin7	|- Fin7 = { x | -. E. y e. ( On \ _om ) x ~~ y }
5	3 4	elab2g	|- ( A e. V -> ( A e. Fin7 <-> -. E. y e. ( On \ _om ) A ~~ y ) )