Theorem afv2eq12d

Description: Equality deduction for function value, analogous to fveq12d . (Contributed by AV, 4-Sep-2022)

	Ref	Expression
Hypotheses	afv2eq12d.1	|- ( ph -> F = G )
	afv2eq12d.2	|- ( ph -> A = B )
Assertion	afv2eq12d	|- ( ph -> ( F '''' A ) = ( G '''' B ) )

Proof

Step	Hyp	Ref	Expression
1		afv2eq12d.1	|- ( ph -> F = G )
2		afv2eq12d.2	|- ( ph -> A = B )
3	1 2	dfateq12d	|- ( ph -> ( F defAt A <-> G defAt B ) )
4		eqidd	|- ( ph -> x = x )
5	2 1 4	breq123d	|- ( ph -> ( A F x <-> B G x ) )
6	5	iotabidv	|- ( ph -> ( iota x A F x ) = ( iota x B G x ) )
7	1	rneqd	|- ( ph -> ran F = ran G )
8	7	unieqd	|- ( ph -> U. ran F = U. ran G )
9	8	pweqd	|- ( ph -> ~P U. ran F = ~P U. ran G )
10	3 6 9	ifbieq12d	|- ( ph -> if ( F defAt A , ( iota x A F x ) , ~P U. ran F ) = if ( G defAt B , ( iota x B G x ) , ~P U. ran G ) )
11		df-afv2	|- ( F '''' A ) = if ( F defAt A , ( iota x A F x ) , ~P U. ran F )
12		df-afv2	|- ( G '''' B ) = if ( G defAt B , ( iota x B G x ) , ~P U. ran G )
13	10 11 12	3eqtr4g	|- ( ph -> ( F '''' A ) = ( G '''' B ) )