Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fnbrafvb Structured version   Visualization version   GIF version

Theorem fnbrafvb 42738
Description: Equivalence of function value and binary relation, analogous to fnbrfvb 6546. (Contributed by Alexander van der Vekens, 25-May-2017.)
Assertion
Ref Expression
fnbrafvb ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹'''𝐵) = 𝐶𝐵𝐹𝐶))

Proof of Theorem fnbrafvb
StepHypRef Expression
1 fndm 6286 . . . . . 6 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
2 eleq2 2851 . . . . . . . 8 (𝐴 = dom 𝐹 → (𝐵𝐴𝐵 ∈ dom 𝐹))
32eqcoms 2783 . . . . . . 7 (dom 𝐹 = 𝐴 → (𝐵𝐴𝐵 ∈ dom 𝐹))
43biimpd 221 . . . . . 6 (dom 𝐹 = 𝐴 → (𝐵𝐴𝐵 ∈ dom 𝐹))
51, 4syl 17 . . . . 5 (𝐹 Fn 𝐴 → (𝐵𝐴𝐵 ∈ dom 𝐹))
65imp 398 . . . 4 ((𝐹 Fn 𝐴𝐵𝐴) → 𝐵 ∈ dom 𝐹)
7 snssi 4613 . . . . . . 7 (𝐵𝐴 → {𝐵} ⊆ 𝐴)
87adantl 474 . . . . . 6 ((𝐹 Fn 𝐴𝐵𝐴) → {𝐵} ⊆ 𝐴)
9 fnssresb 6300 . . . . . . 7 (𝐹 Fn 𝐴 → ((𝐹 ↾ {𝐵}) Fn {𝐵} ↔ {𝐵} ⊆ 𝐴))
109adantr 473 . . . . . 6 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹 ↾ {𝐵}) Fn {𝐵} ↔ {𝐵} ⊆ 𝐴))
118, 10mpbird 249 . . . . 5 ((𝐹 Fn 𝐴𝐵𝐴) → (𝐹 ↾ {𝐵}) Fn {𝐵})
12 fnfun 6284 . . . . 5 ((𝐹 ↾ {𝐵}) Fn {𝐵} → Fun (𝐹 ↾ {𝐵}))
1311, 12syl 17 . . . 4 ((𝐹 Fn 𝐴𝐵𝐴) → Fun (𝐹 ↾ {𝐵}))
14 df-dfat 42703 . . . . 5 (𝐹 defAt 𝐵 ↔ (𝐵 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐵})))
15 afvfundmfveq 42722 . . . . 5 (𝐹 defAt 𝐵 → (𝐹'''𝐵) = (𝐹𝐵))
1614, 15sylbir 227 . . . 4 ((𝐵 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐵})) → (𝐹'''𝐵) = (𝐹𝐵))
176, 13, 16syl2anc 576 . . 3 ((𝐹 Fn 𝐴𝐵𝐴) → (𝐹'''𝐵) = (𝐹𝐵))
1817eqeq1d 2777 . 2 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹'''𝐵) = 𝐶 ↔ (𝐹𝐵) = 𝐶))
19 fnbrfvb 6546 . 2 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) = 𝐶𝐵𝐹𝐶))
2018, 19bitrd 271 1 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹'''𝐵) = 𝐶𝐵𝐹𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387   = wceq 1507  wcel 2048  wss 3828  {csn 4439   class class class wbr 4927  dom cdm 5404  cres 5406  Fun wfun 6180   Fn wfn 6181  cfv 6186   defAt wdfat 42700  '''cafv 42701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-sep 5058  ax-nul 5065  ax-pow 5117  ax-pr 5184
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ne 2965  df-ral 3090  df-rex 3091  df-rab 3094  df-v 3414  df-sbc 3681  df-csb 3786  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-nul 4178  df-if 4349  df-sn 4440  df-pr 4442  df-op 4446  df-uni 4711  df-int 4748  df-br 4928  df-opab 4990  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-res 5416  df-iota 6150  df-fun 6188  df-fn 6189  df-fv 6194  df-aiota 42670  df-dfat 42703  df-afv 42704
This theorem is referenced by:  fnopafvb  42739  funbrafvb  42740  dfafn5a  42744
  Copyright terms: Public domain W3C validator