Theorem onsetreclem1

Description: Lemma for onsetrec . (Contributed by Emmett Weisz, 22-Jun-2021) (New usage is discouraged.)

	Ref	Expression
Hypothesis	onsetreclem1.1	|- F = ( x e. _V |-> { U. x , suc U. x } )
Assertion	onsetreclem1	|- ( F ` a ) = { U. a , suc U. a }

Proof

Step	Hyp	Ref	Expression
1		onsetreclem1.1	|- F = ( x e. _V |-> { U. x , suc U. x } )
2		unieq	|- ( x = a -> U. x = U. a )
3		suceq	|- ( U. x = U. a -> suc U. x = suc U. a )
4	2 3	syl	|- ( x = a -> suc U. x = suc U. a )
5	2 4	preq12d	|- ( x = a -> { U. x , suc U. x } = { U. a , suc U. a } )
6		prex	|- { U. a , suc U. a } e. _V
7	5 1 6	fvmpt	|- ( a e. _V -> ( F ` a ) = { U. a , suc U. a } )
8	7	elv	|- ( F ` a ) = { U. a , suc U. a }