Theorem mpteqb 5204

Description: Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnfv 5208. (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 2560	. . 3 |- (B e. V -> B e. _V)
2	1	ralimi 2378	. 2 |- (A.x e. A B e. V -> A.x e. A B e. _V)
3		fneq1 4930	. . . . . . 7 |- ((x e. A |-> B) = (x e. A |-> C) -> ((x e. A |-> B) Fn A <-> (x e. A |-> C) Fn A))
4		eqid 2037	. . . . . . . 8 |- (x e. A |-> B) = (x e. A |-> B)
5	4	mptfng 4967	. . . . . . 7 |- (A.x e. A B e. _V <-> (x e. A |-> B) Fn A)
6		eqid 2037	. . . . . . . 8 |- (x e. A |-> C) = (x e. A |-> C)
7	6	mptfng 4967	. . . . . . 7 |- (A.x e. A C e. _V <-> (x e. A |-> C) Fn A)
8	3, 5, 7	3bitr4g 212	. . . . . 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 132	. . . . 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 2435	. . . . . . 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 3841	. . . . . . . . . 10 |- F/_x(x e. A |-> B)
12		nfmpt1 3841	. . . . . . . . . 10 |- F/_x(x e. A |-> C)
13	11, 12	nfeq 2182	. . . . . . . . 9 |- F/x(x e. A |-> B) = (x e. A |-> C)
14		simpll 481	. . . . . . . . . . . 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 5123	. . . . . . . . . . 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 5197	. . . . . . . . . . . 12 |- ((x e. A /\ B e. _V) -> ((x e. A |-> B) ` x) = B)
17	16	ad2ant2lr 479	. . . . . . . . . . 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 5197	. . . . . . . . . . . 12 |- ((x e. A /\ C e. _V) -> ((x e. A |-> C) ` x) = C)
19	18	ad2ant2l 477	. . . . . . . . . . 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 2077	. . . . . . . . . 10 |- ((((x e. A |-> B) = (x e. A |-> C) /\ x e. A) /\ (B e. _V /\ C e. _V)) -> B = C)
21	20	exp31 346	. . . . . . . . 9 |- ((x e. A |-> B) = (x e. A |-> C) -> (x e. A -> ((B e. _V /\ C e. _V) -> B = C)))
22	13, 21	ralrimi 2384	. . . . . . . 8 |- ((x e. A |-> B) = (x e. A |-> C) -> A.x e. A ((B e. _V /\ C e. _V) -> B = C))
23		ralim 2374	. . . . . . . 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 14	. . . . . . 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 142	. . . . . 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 245	. . . . 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 36	. . . 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 27	. . 3 |- (A.x e. A B e. _V -> ((x e. A |-> B) = (x e. A |-> C) -> A.x e. A B = C))
29		eqid 2037	. . . 4 |- A = A
30		mpteq12 3831	. . . 4 |- ((A = A /\ A.x e. A B = C) -> (x e. A |-> B) = (x e. A |-> C))
31	29, 30	mpan 400	. . 3 |- (A.x e. A B = C -> (x e. A |-> B) = (x e. A |-> C))
32	28, 31	impbid1 130	. 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 14	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   /\ wa 97   <-> wb 98   = wceq 1242   e. wcel 1390  A.wral 2300   _Vcvv 2551   |-> cmpt 3809   Fn wfn 4840   ` cfv 4845

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-csb 2847  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-iota 4810  df-fun 4847  df-fn 4848  df-fv 4853

This theorem is referenced by:  eqfnfv  5208  eufnfv  5332  offveqb  5672