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

Theorem mpteqb 6096
Description: Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnfv 6108. (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 3089 . . 3 (𝐵𝑉𝐵 ∈ V)
21ralimi 2840 . 2 (∀𝑥𝐴 𝐵𝑉 → ∀𝑥𝐴 𝐵 ∈ V)
3 fneq1 5783 . . . . . . 7 ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) → ((𝑥𝐴𝐵) Fn 𝐴 ↔ (𝑥𝐴𝐶) Fn 𝐴))
4 eqid 2514 . . . . . . . 8 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
54mptfng 5822 . . . . . . 7 (∀𝑥𝐴 𝐵 ∈ V ↔ (𝑥𝐴𝐵) Fn 𝐴)
6 eqid 2514 . . . . . . . 8 (𝑥𝐴𝐶) = (𝑥𝐴𝐶)
76mptfng 5822 . . . . . . 7 (∀𝑥𝐴 𝐶 ∈ V ↔ (𝑥𝐴𝐶) Fn 𝐴)
83, 5, 73bitr4g 301 . . . . . 6 ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) → (∀𝑥𝐴 𝐵 ∈ V ↔ ∀𝑥𝐴 𝐶 ∈ V))
98biimpd 217 . . . . 5 ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) → (∀𝑥𝐴 𝐵 ∈ V → ∀𝑥𝐴 𝐶 ∈ V))
10 r19.26 2950 . . . . . . 7 (∀𝑥𝐴 (𝐵 ∈ V ∧ 𝐶 ∈ V) ↔ (∀𝑥𝐴 𝐵 ∈ V ∧ ∀𝑥𝐴 𝐶 ∈ V))
11 nfmpt1 4573 . . . . . . . . . 10 𝑥(𝑥𝐴𝐵)
12 nfmpt1 4573 . . . . . . . . . 10 𝑥(𝑥𝐴𝐶)
1311, 12nfeq 2666 . . . . . . . . 9 𝑥(𝑥𝐴𝐵) = (𝑥𝐴𝐶)
14 simpll 785 . . . . . . . . . . . 12 ((((𝑥𝐴𝐵) = (𝑥𝐴𝐶) ∧ 𝑥𝐴) ∧ (𝐵 ∈ V ∧ 𝐶 ∈ V)) → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
1514fveq1d 5994 . . . . . . . . . . 11 ((((𝑥𝐴𝐵) = (𝑥𝐴𝐶) ∧ 𝑥𝐴) ∧ (𝐵 ∈ V ∧ 𝐶 ∈ V)) → ((𝑥𝐴𝐵)‘𝑥) = ((𝑥𝐴𝐶)‘𝑥))
164fvmpt2 6089 . . . . . . . . . . . 12 ((𝑥𝐴𝐵 ∈ V) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
1716ad2ant2lr 779 . . . . . . . . . . 11 ((((𝑥𝐴𝐵) = (𝑥𝐴𝐶) ∧ 𝑥𝐴) ∧ (𝐵 ∈ V ∧ 𝐶 ∈ V)) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
186fvmpt2 6089 . . . . . . . . . . . 12 ((𝑥𝐴𝐶 ∈ V) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
1918ad2ant2l 777 . . . . . . . . . . 11 ((((𝑥𝐴𝐵) = (𝑥𝐴𝐶) ∧ 𝑥𝐴) ∧ (𝐵 ∈ V ∧ 𝐶 ∈ V)) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
2015, 17, 193eqtr3d 2556 . . . . . . . . . 10 ((((𝑥𝐴𝐵) = (𝑥𝐴𝐶) ∧ 𝑥𝐴) ∧ (𝐵 ∈ V ∧ 𝐶 ∈ V)) → 𝐵 = 𝐶)
2120exp31 627 . . . . . . . . 9 ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) → (𝑥𝐴 → ((𝐵 ∈ V ∧ 𝐶 ∈ V) → 𝐵 = 𝐶)))
2213, 21ralrimi 2844 . . . . . . . 8 ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) → ∀𝑥𝐴 ((𝐵 ∈ V ∧ 𝐶 ∈ V) → 𝐵 = 𝐶))
23 ralim 2836 . . . . . . . 8 (∀𝑥𝐴 ((𝐵 ∈ V ∧ 𝐶 ∈ V) → 𝐵 = 𝐶) → (∀𝑥𝐴 (𝐵 ∈ V ∧ 𝐶 ∈ V) → ∀𝑥𝐴 𝐵 = 𝐶))
2422, 23syl 17 . . . . . . 7 ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) → (∀𝑥𝐴 (𝐵 ∈ V ∧ 𝐶 ∈ V) → ∀𝑥𝐴 𝐵 = 𝐶))
2510, 24syl5bir 231 . . . . . 6 ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) → ((∀𝑥𝐴 𝐵 ∈ V ∧ ∀𝑥𝐴 𝐶 ∈ V) → ∀𝑥𝐴 𝐵 = 𝐶))
2625expd 450 . . . . 5 ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) → (∀𝑥𝐴 𝐵 ∈ V → (∀𝑥𝐴 𝐶 ∈ V → ∀𝑥𝐴 𝐵 = 𝐶)))
279, 26mpdd 41 . . . 4 ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) → (∀𝑥𝐴 𝐵 ∈ V → ∀𝑥𝐴 𝐵 = 𝐶))
2827com12 32 . . 3 (∀𝑥𝐴 𝐵 ∈ V → ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) → ∀𝑥𝐴 𝐵 = 𝐶))
29 eqid 2514 . . . 4 𝐴 = 𝐴
30 mpteq12 4562 . . . 4 ((𝐴 = 𝐴 ∧ ∀𝑥𝐴 𝐵 = 𝐶) → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
3129, 30mpan 701 . . 3 (∀𝑥𝐴 𝐵 = 𝐶 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
3228, 31impbid1 213 . 2 (∀𝑥𝐴 𝐵 ∈ V → ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) ↔ ∀𝑥𝐴 𝐵 = 𝐶))
332, 32syl 17 1 (∀𝑥𝐴 𝐵𝑉 → ((𝑥𝐴𝐵) = (𝑥𝐴𝐶) ↔ ∀𝑥𝐴 𝐵 = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1938  wral 2800  Vcvv 3077  cmpt 4541   Fn wfn 5689  cfv 5694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-br 4482  df-opab 4542  df-mpt 4543  df-id 4847  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-iota 5658  df-fun 5696  df-fn 5697  df-fv 5702
This theorem is referenced by:  eqfnfv  6108  eufnfv  6277  offveqb  6698  ramcl  15459  fucsect  16351  setcepi  16457  0frgp  17927  dprdf11  18156  dpjeq  18192  mvrf1  19154  mplmonmul  19193  frgpcyg  19651  ustuqtop  21767  mdegle0  23520  ply1nzb  23565  cvmliftphtlem  30402  matunitlindflem1  32469
  Copyright terms: Public domain W3C validator