Theorem mpteqb 6891

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

Assertion

Ref	Expression
mpteqb	⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶))

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝑉(𝑥)

Proof of Theorem mpteqb

Step	Hyp	Ref	Expression
1		elex 3449	. . 3 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
2	1	ralimi 3089	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
3		fneq1 6522	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) → ((𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ 𝐶) Fn 𝐴))
4		eqid 2740	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
5	4	mptfng 6570	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴)
6		eqid 2740	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ 𝐶)
7	6	mptfng 6570	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ V ↔ (𝑥 ∈ 𝐴 ↦ 𝐶) Fn 𝐴)
8	3, 5, 7	3bitr4g 314	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) → (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ V))
9	8	biimpd 228	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) → (∀𝑥 ∈ 𝐴 𝐵 ∈ V → ∀𝑥 ∈ 𝐴 𝐶 ∈ V))
10		r19.26 3097	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐵 ∈ V ∧ 𝐶 ∈ V) ↔ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ∧ ∀𝑥 ∈ 𝐴 𝐶 ∈ V))
11		nfmpt1 5187	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)
12		nfmpt1 5187	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐶)
13	11, 12	nfeq 2922	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)
14		simpll 764	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) ∧ 𝑥 ∈ 𝐴) ∧ (𝐵 ∈ V ∧ 𝐶 ∈ V)) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
15	14	fveq1d 6773	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) ∧ 𝑥 ∈ 𝐴) ∧ (𝐵 ∈ V ∧ 𝐶 ∈ V)) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥))
16	4	fvmpt2 6883	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ V) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
17	16	ad2ant2lr 745	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) ∧ 𝑥 ∈ 𝐴) ∧ (𝐵 ∈ V ∧ 𝐶 ∈ V)) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
18	6	fvmpt2 6883	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ V) → ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥) = 𝐶)
19	18	ad2ant2l 743	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) ∧ 𝑥 ∈ 𝐴) ∧ (𝐵 ∈ V ∧ 𝐶 ∈ V)) → ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥) = 𝐶)
20	15, 17, 19	3eqtr3d 2788	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) ∧ 𝑥 ∈ 𝐴) ∧ (𝐵 ∈ V ∧ 𝐶 ∈ V)) → 𝐵 = 𝐶)
21	20	exp31 420	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) → (𝑥 ∈ 𝐴 → ((𝐵 ∈ V ∧ 𝐶 ∈ V) → 𝐵 = 𝐶)))
22	13, 21	ralrimi 3142	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) → ∀𝑥 ∈ 𝐴 ((𝐵 ∈ V ∧ 𝐶 ∈ V) → 𝐵 = 𝐶))
23		ralim 3085	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 ((𝐵 ∈ V ∧ 𝐶 ∈ V) → 𝐵 = 𝐶) → (∀𝑥 ∈ 𝐴 (𝐵 ∈ V ∧ 𝐶 ∈ V) → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶))
24	22, 23	syl 17	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) → (∀𝑥 ∈ 𝐴 (𝐵 ∈ V ∧ 𝐶 ∈ V) → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶))
25	10, 24	syl5bir 242	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) → ((∀𝑥 ∈ 𝐴 𝐵 ∈ V ∧ ∀𝑥 ∈ 𝐴 𝐶 ∈ V) → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶))
26	25	expd 416	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) → (∀𝑥 ∈ 𝐴 𝐵 ∈ V → (∀𝑥 ∈ 𝐴 𝐶 ∈ V → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶)))
27	9, 26	mpdd 43	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) → (∀𝑥 ∈ 𝐴 𝐵 ∈ V → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶))
28	27	com12 32	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V → ((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶))
29		eqid 2740	. . . 4 ⊢ 𝐴 = 𝐴
30		mpteq12 5171	. . . 4 ⊢ ((𝐴 = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
31	29, 30	mpan 687	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
32	28, 31	impbid1 224	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V → ((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶))
33	2, 32	syl 17	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1542   ∈ wcel 2110  ∀wral 3066  Vcvv 3431   ↦ cmpt 5162   Fn wfn 6427  ‘cfv 6432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6390  df-fun 6434  df-fn 6435  df-fv 6440

This theorem is referenced by:  eqfnfv  6906  eufnfv  7102  offveqb  7552  ramcl  16728  fucsect  17688  setcepi  17801  0frgp  19383  dprdf11  19624  dpjeq  19660  frgpcyg  20779  mvrf1  21192  mplmonmul  21235  ustuqtop  23396  mdegle0  25240  ply1nzb  25285  fedgmullem2  31707  cvmliftphtlem  33275  matunitlindflem1  35769  cfsetsnfsetf1  44521  1arymaptf1  45957