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

Theorem fnbrfvb 6377
Description: Equivalence of function value and binary relation. (Contributed by NM, 19-Apr-2004.) (Revised by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
fnbrfvb ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) = 𝐶𝐵𝐹𝐶))

Proof of Theorem fnbrfvb
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 eqid 2771 . . . 4 (𝐹𝐵) = (𝐹𝐵)
2 fvex 6342 . . . . 5 (𝐹𝐵) ∈ V
3 eqeq2 2782 . . . . . . 7 (𝑥 = (𝐹𝐵) → ((𝐹𝐵) = 𝑥 ↔ (𝐹𝐵) = (𝐹𝐵)))
4 breq2 4790 . . . . . . 7 (𝑥 = (𝐹𝐵) → (𝐵𝐹𝑥𝐵𝐹(𝐹𝐵)))
53, 4bibi12d 334 . . . . . 6 (𝑥 = (𝐹𝐵) → (((𝐹𝐵) = 𝑥𝐵𝐹𝑥) ↔ ((𝐹𝐵) = (𝐹𝐵) ↔ 𝐵𝐹(𝐹𝐵))))
65imbi2d 329 . . . . 5 (𝑥 = (𝐹𝐵) → (((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) = 𝑥𝐵𝐹𝑥)) ↔ ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) = (𝐹𝐵) ↔ 𝐵𝐹(𝐹𝐵)))))
7 fneu 6135 . . . . . 6 ((𝐹 Fn 𝐴𝐵𝐴) → ∃!𝑥 𝐵𝐹𝑥)
8 tz6.12c 6354 . . . . . 6 (∃!𝑥 𝐵𝐹𝑥 → ((𝐹𝐵) = 𝑥𝐵𝐹𝑥))
97, 8syl 17 . . . . 5 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) = 𝑥𝐵𝐹𝑥))
102, 6, 9vtocl 3410 . . . 4 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) = (𝐹𝐵) ↔ 𝐵𝐹(𝐹𝐵)))
111, 10mpbii 223 . . 3 ((𝐹 Fn 𝐴𝐵𝐴) → 𝐵𝐹(𝐹𝐵))
12 breq2 4790 . . 3 ((𝐹𝐵) = 𝐶 → (𝐵𝐹(𝐹𝐵) ↔ 𝐵𝐹𝐶))
1311, 12syl5ibcom 235 . 2 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) = 𝐶𝐵𝐹𝐶))
14 fnfun 6128 . . . 4 (𝐹 Fn 𝐴 → Fun 𝐹)
15 funbrfv 6375 . . . 4 (Fun 𝐹 → (𝐵𝐹𝐶 → (𝐹𝐵) = 𝐶))
1614, 15syl 17 . . 3 (𝐹 Fn 𝐴 → (𝐵𝐹𝐶 → (𝐹𝐵) = 𝐶))
1716adantr 466 . 2 ((𝐹 Fn 𝐴𝐵𝐴) → (𝐵𝐹𝐶 → (𝐹𝐵) = 𝐶))
1813, 17impbid 202 1 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) = 𝐶𝐵𝐹𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  ∃!weu 2618   class class class wbr 4786  Fun wfun 6025   Fn wfn 6026  cfv 6031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-iota 5994  df-fun 6033  df-fn 6034  df-fv 6039
This theorem is referenced by:  fnopfvb  6378  funbrfvb  6379  fnbrfvb2  6381  dffn5  6383  feqmptdf  6393  fnsnfv  6400  fndmdif  6464  dffo4  6518  dff13  6655  isomin  6730  isoini  6731  br1steqg  7337  br2ndeqg  7338  1stconst  7416  2ndconst  7417  fsplit  7433  seqomlem3  7700  seqomlem4  7701  nqerrel  9956  imasleval  16409  znleval  20118  axcontlem5  26069  elnlfn  29127  adjbd1o  29284  fcoinvbr  29757  elintfv  32000  fv1stcnv  32016  fv2ndcnv  32017  trpredpred  32064  scutun12  32254  madeval2  32273  fvbigcup  32346  fvsingle  32364  imageval  32374  brfullfun  32392  bj-mptval  33402  unccur  33725  poimirlem2  33744  poimirlem23  33765  pw2f1ocnv  38130  brcoffn  38854  funressnfv  41728  fnbrafvb  41754
  Copyright terms: Public domain W3C validator