MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpteqb Structured version   Visualization version   GIF version

Theorem mpteqb 6453
Description: Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnfv 6466. (Contributed by Mario Carneiro, 14-Nov-2014.)
Assertion
Ref Expression
mpteqb (∀𝑥𝐴 𝐵𝑉 → ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) ↔ ∀𝑥𝐴 𝐵 = 𝐶))
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝑉(𝑥)

Proof of Theorem mpteqb
StepHypRef Expression
1 elex 3344 . . 3 (𝐵𝑉𝐵 ∈ V)
21ralimi 3082 . 2 (∀𝑥𝐴 𝐵𝑉 → ∀𝑥𝐴 𝐵 ∈ V)
3 fneq1 6132 . . . . . . 7 ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) → ((𝑥𝐴𝐵) Fn 𝐴 ↔ (𝑥𝐴𝐶) Fn 𝐴))
4 eqid 2752 . . . . . . . 8 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
54mptfng 6172 . . . . . . 7 (∀𝑥𝐴 𝐵 ∈ V ↔ (𝑥𝐴𝐵) Fn 𝐴)
6 eqid 2752 . . . . . . . 8 (𝑥𝐴𝐶) = (𝑥𝐴𝐶)
76mptfng 6172 . . . . . . 7 (∀𝑥𝐴 𝐶 ∈ V ↔ (𝑥𝐴𝐶) Fn 𝐴)
83, 5, 73bitr4g 303 . . . . . 6 ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) → (∀𝑥𝐴 𝐵 ∈ V ↔ ∀𝑥𝐴 𝐶 ∈ V))
98biimpd 219 . . . . 5 ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) → (∀𝑥𝐴 𝐵 ∈ V → ∀𝑥𝐴 𝐶 ∈ V))
10 r19.26 3194 . . . . . . 7 (∀𝑥𝐴 (𝐵 ∈ V ∧ 𝐶 ∈ V) ↔ (∀𝑥𝐴 𝐵 ∈ V ∧ ∀𝑥𝐴 𝐶 ∈ V))
11 nfmpt1 4891 . . . . . . . . . 10 𝑥(𝑥𝐴𝐵)
12 nfmpt1 4891 . . . . . . . . . 10 𝑥(𝑥𝐴𝐶)
1311, 12nfeq 2906 . . . . . . . . 9 𝑥(𝑥𝐴𝐵) = (𝑥𝐴𝐶)
14 simpll 807 . . . . . . . . . . . 12 ((((𝑥𝐴𝐵) = (𝑥𝐴𝐶) ∧ 𝑥𝐴) ∧ (𝐵 ∈ V ∧ 𝐶 ∈ V)) → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
1514fveq1d 6346 . . . . . . . . . . 11 ((((𝑥𝐴𝐵) = (𝑥𝐴𝐶) ∧ 𝑥𝐴) ∧ (𝐵 ∈ V ∧ 𝐶 ∈ V)) → ((𝑥𝐴𝐵)‘𝑥) = ((𝑥𝐴𝐶)‘𝑥))
164fvmpt2 6445 . . . . . . . . . . . 12 ((𝑥𝐴𝐵 ∈ V) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
1716ad2ant2lr 801 . . . . . . . . . . 11 ((((𝑥𝐴𝐵) = (𝑥𝐴𝐶) ∧ 𝑥𝐴) ∧ (𝐵 ∈ V ∧ 𝐶 ∈ V)) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
186fvmpt2 6445 . . . . . . . . . . . 12 ((𝑥𝐴𝐶 ∈ V) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
1918ad2ant2l 799 . . . . . . . . . . 11 ((((𝑥𝐴𝐵) = (𝑥𝐴𝐶) ∧ 𝑥𝐴) ∧ (𝐵 ∈ V ∧ 𝐶 ∈ V)) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
2015, 17, 193eqtr3d 2794 . . . . . . . . . 10 ((((𝑥𝐴𝐵) = (𝑥𝐴𝐶) ∧ 𝑥𝐴) ∧ (𝐵 ∈ V ∧ 𝐶 ∈ V)) → 𝐵 = 𝐶)
2120exp31 631 . . . . . . . . 9 ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) → (𝑥𝐴 → ((𝐵 ∈ V ∧ 𝐶 ∈ V) → 𝐵 = 𝐶)))
2213, 21ralrimi 3087 . . . . . . . 8 ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) → ∀𝑥𝐴 ((𝐵 ∈ V ∧ 𝐶 ∈ V) → 𝐵 = 𝐶))
23 ralim 3078 . . . . . . . 8 (∀𝑥𝐴 ((𝐵 ∈ V ∧ 𝐶 ∈ V) → 𝐵 = 𝐶) → (∀𝑥𝐴 (𝐵 ∈ V ∧ 𝐶 ∈ V) → ∀𝑥𝐴 𝐵 = 𝐶))
2422, 23syl 17 . . . . . . 7 ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) → (∀𝑥𝐴 (𝐵 ∈ V ∧ 𝐶 ∈ V) → ∀𝑥𝐴 𝐵 = 𝐶))
2510, 24syl5bir 233 . . . . . 6 ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) → ((∀𝑥𝐴 𝐵 ∈ V ∧ ∀𝑥𝐴 𝐶 ∈ V) → ∀𝑥𝐴 𝐵 = 𝐶))
2625expd 451 . . . . 5 ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) → (∀𝑥𝐴 𝐵 ∈ V → (∀𝑥𝐴 𝐶 ∈ V → ∀𝑥𝐴 𝐵 = 𝐶)))
279, 26mpdd 43 . . . 4 ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) → (∀𝑥𝐴 𝐵 ∈ V → ∀𝑥𝐴 𝐵 = 𝐶))
2827com12 32 . . 3 (∀𝑥𝐴 𝐵 ∈ V → ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) → ∀𝑥𝐴 𝐵 = 𝐶))
29 eqid 2752 . . . 4 𝐴 = 𝐴
30 mpteq12 4880 . . . 4 ((𝐴 = 𝐴 ∧ ∀𝑥𝐴 𝐵 = 𝐶) → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
3129, 30mpan 708 . . 3 (∀𝑥𝐴 𝐵 = 𝐶 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
3228, 31impbid1 215 . 2 (∀𝑥𝐴 𝐵 ∈ V → ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) ↔ ∀𝑥𝐴 𝐵 = 𝐶))
332, 32syl 17 1 (∀𝑥𝐴 𝐵𝑉 → ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) ↔ ∀𝑥𝐴 𝐵 = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1624  wcel 2131  wral 3042  Vcvv 3332  cmpt 4873   Fn wfn 6036  cfv 6041
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-opab 4857  df-mpt 4874  df-id 5166  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-iota 6004  df-fun 6043  df-fn 6044  df-fv 6049
This theorem is referenced by:  eqfnfv  6466  eufnfv  6646  offveqb  7076  ramcl  15927  fucsect  16825  setcepi  16931  0frgp  18384  dprdf11  18614  dpjeq  18650  mvrf1  19619  mplmonmul  19658  frgpcyg  20116  ustuqtop  22243  mdegle0  24028  ply1nzb  24073  cvmliftphtlem  31598  matunitlindflem1  33710
  Copyright terms: Public domain W3C validator