Theorem mpteqb 5964

Description: Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnfv 5975. (Contributed by Mario Carneiro, 14-Nov-2014.)

Assertion

Ref	Expression
mpteqb	|- ( A. x e. A B e. V -> ( ( x e. A |-> B ) = ( x e. A |-> C ) <-> A. x e. A B = C ) )

Distinct variable group:   x, A

Allowed substitution hints:   B( x)   C( x)   V( x)

Proof of Theorem mpteqb

Step	Hyp	Ref	Expression
1		elex 3122	. . 3 |- ( B e. V -> B e. _V )
2	1	ralimi 2857	. 2 |- ( A. x e. A B e. V -> A. x e. A B e. _V )
3		fneq1 5669	. . . . . . 7 |- ( ( x e. A |-> B ) = ( x e. A |-> C ) -> ( ( x e. A |-> B ) Fn A <-> ( x e. A |-> C ) Fn A ) )
4		eqid 2467	. . . . . . . 8 |- ( x e. A |-> B ) = ( x e. A |-> B )
5	4	mptfng 5706	. . . . . . 7 |- ( A. x e. A B e. _V <-> ( x e. A |-> B ) Fn A )
6		eqid 2467	. . . . . . . 8 |- ( x e. A |-> C ) = ( x e. A |-> C )
7	6	mptfng 5706	. . . . . . 7 |- ( A. x e. A C e. _V <-> ( x e. A |-> C ) Fn A )
8	3, 5, 7	3bitr4g 288	. . . . . 6 |- ( ( x e. A |-> B ) = ( x e. A |-> C ) -> ( A. x e. A B e. _V <-> A. x e. A C e. _V ) )
9	8	biimpd 207	. . . . 5 |- ( ( x e. A |-> B ) = ( x e. A |-> C ) -> ( A. x e. A B e. _V -> A. x e. A C e. _V ) )
10		r19.26 2989	. . . . . . 7 |- ( A. x e. A ( B e. _V /\ C e. _V ) <-> ( A. x e. A B e. _V /\ A. x e. A C e. _V ) )
11		nfmpt1 4536	. . . . . . . . . 10 |- F/_ x ( x e. A |-> B )
12		nfmpt1 4536	. . . . . . . . . 10 |- F/_ x ( x e. A |-> C )
13	11, 12	nfeq 2640	. . . . . . . . 9 |- F/ x ( x e. A |-> B ) = ( x e. A |-> C )
14		simpll 753	. . . . . . . . . . . 12 |- ( ( ( ( x e. A |-> B ) = ( x e. A |-> C ) /\ x e. A ) /\ ( B e. _V /\ C e. _V ) ) -> ( x e. A |-> B ) = ( x e. A |-> C ) )
15	14	fveq1d 5868	. . . . . . . . . . 11 |- ( ( ( ( x e. A |-> B ) = ( x e. A |-> C ) /\ x e. A ) /\ ( B e. _V /\ C e. _V ) ) -> ( ( x e. A |-> B ) ` x ) = ( ( x e. A |-> C ) ` x ) )
16	4	fvmpt2 5957	. . . . . . . . . . . 12 |- ( ( x e. A /\ B e. _V ) -> ( ( x e. A |-> B ) ` x ) = B )
17	16	ad2ant2lr 747	. . . . . . . . . . 11 |- ( ( ( ( x e. A |-> B ) = ( x e. A |-> C ) /\ x e. A ) /\ ( B e. _V /\ C e. _V ) ) -> ( ( x e. A |-> B ) ` x ) = B )
18	6	fvmpt2 5957	. . . . . . . . . . . 12 |- ( ( x e. A /\ C e. _V ) -> ( ( x e. A |-> C ) ` x ) = C )
19	18	ad2ant2l 745	. . . . . . . . . . 11 |- ( ( ( ( x e. A |-> B ) = ( x e. A |-> C ) /\ x e. A ) /\ ( B e. _V /\ C e. _V ) ) -> ( ( x e. A |-> C ) ` x ) = C )
20	15, 17, 19	3eqtr3d 2516	. . . . . . . . . 10 |- ( ( ( ( x e. A |-> B ) = ( x e. A |-> C ) /\ x e. A ) /\ ( B e. _V /\ C e. _V ) ) -> B = C )
21	20	exp31 604	. . . . . . . . 9 |- ( ( x e. A |-> B ) = ( x e. A |-> C ) -> ( x e. A -> ( ( B e. _V /\ C e. _V ) -> B = C ) ) )
22	13, 21	ralrimi 2864	. . . . . . . 8 |- ( ( x e. A |-> B ) = ( x e. A |-> C ) -> A. x e. A ( ( B e. _V /\ C e. _V ) -> B = C ) )
23		ralim 2853	. . . . . . . 8 |- ( A. x e. A ( ( B e. _V /\ C e. _V ) -> B = C ) -> ( A. x e. A ( B e. _V /\ C e. _V ) -> A. x e. A B = C ) )
24	22, 23	syl 16	. . . . . . 7 |- ( ( x e. A |-> B ) = ( x e. A |-> C ) -> ( A. x e. A ( B e. _V /\ C e. _V ) -> A. x e. A B = C ) )
25	10, 24	syl5bir 218	. . . . . 6 |- ( ( x e. A |-> B ) = ( x e. A |-> C ) -> ( ( A. x e. A B e. _V /\ A. x e. A C e. _V ) -> A. x e. A B = C ) )
26	25	expd 436	. . . . 5 |- ( ( x e. A |-> B ) = ( x e. A |-> C ) -> ( A. x e. A B e. _V -> ( A. x e. A C e. _V -> A. x e. A B = C ) ) )
27	9, 26	mpdd 40	. . . 4 |- ( ( x e. A |-> B ) = ( x e. A |-> C ) -> ( A. x e. A B e. _V -> A. x e. A B = C ) )
28	27	com12 31	. . 3 |- ( A. x e. A B e. _V -> ( ( x e. A |-> B ) = ( x e. A |-> C ) -> A. x e. A B = C ) )
29		eqid 2467	. . . 4 |- A = A
30		mpteq12 4526	. . . 4 |- ( ( A = A /\ A. x e. A B = C ) -> ( x e. A |-> B ) = ( x e. A |-> C ) )
31	29, 30	mpan 670	. . 3 |- ( A. x e. A B = C -> ( x e. A |-> B ) = ( x e. A |-> C ) )
32	28, 31	impbid1 203	. 2 |- ( A. x e. A B e. _V -> ( ( x e. A |-> B ) = ( x e. A |-> C ) <-> A. x e. A B = C ) )
33	2, 32	syl 16	1 |- ( A. x e. A B e. V -> ( ( x e. A |-> B ) = ( x e. A |-> C ) <-> A. x e. A B = C ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1379   e. wcel 1767   A.wral 2814   _Vcvv 3113   |-> cmpt 4505   Fn wfn 5583   ` cfv 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-fv 5596

This theorem is referenced by:  eqfnfv  5975  eufnfv  6134  offveqb  6546  ramcl  14406  fucsect  15199  setcepi  15273  0frgp  16603  dprdf11  16865  dprdf11OLD  16872  dpjeq  16910  dpjeqOLD  16917  mvrf1  17880  mplmonmul  17925  frgpcyg  18407  ustuqtop  20512  mdegle0  22240  ply1nzb  22286  cvmliftphtlem  28430