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

Theorem fnbrfvb 6223
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 2620 . . . 4 (𝐹𝐵) = (𝐹𝐵)
2 fvex 6188 . . . . 5 (𝐹𝐵) ∈ V
3 eqeq2 2631 . . . . . . 7 (𝑥 = (𝐹𝐵) → ((𝐹𝐵) = 𝑥 ↔ (𝐹𝐵) = (𝐹𝐵)))
4 breq2 4648 . . . . . . 7 (𝑥 = (𝐹𝐵) → (𝐵𝐹𝑥𝐵𝐹(𝐹𝐵)))
53, 4bibi12d 335 . . . . . 6 (𝑥 = (𝐹𝐵) → (((𝐹𝐵) = 𝑥𝐵𝐹𝑥) ↔ ((𝐹𝐵) = (𝐹𝐵) ↔ 𝐵𝐹(𝐹𝐵))))
65imbi2d 330 . . . . 5 (𝑥 = (𝐹𝐵) → (((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) = 𝑥𝐵𝐹𝑥)) ↔ ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) = (𝐹𝐵) ↔ 𝐵𝐹(𝐹𝐵)))))
7 fneu 5983 . . . . . 6 ((𝐹 Fn 𝐴𝐵𝐴) → ∃!𝑥 𝐵𝐹𝑥)
8 tz6.12c 6200 . . . . . 6 (∃!𝑥 𝐵𝐹𝑥 → ((𝐹𝐵) = 𝑥𝐵𝐹𝑥))
97, 8syl 17 . . . . 5 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) = 𝑥𝐵𝐹𝑥))
102, 6, 9vtocl 3254 . . . 4 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) = (𝐹𝐵) ↔ 𝐵𝐹(𝐹𝐵)))
111, 10mpbii 223 . . 3 ((𝐹 Fn 𝐴𝐵𝐴) → 𝐵𝐹(𝐹𝐵))
12 breq2 4648 . . 3 ((𝐹𝐵) = 𝐶 → (𝐵𝐹(𝐹𝐵) ↔ 𝐵𝐹𝐶))
1311, 12syl5ibcom 235 . 2 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) = 𝐶𝐵𝐹𝐶))
14 fnfun 5976 . . . 4 (𝐹 Fn 𝐴 → Fun 𝐹)
15 funbrfv 6221 . . . 4 (Fun 𝐹 → (𝐵𝐹𝐶 → (𝐹𝐵) = 𝐶))
1614, 15syl 17 . . 3 (𝐹 Fn 𝐴 → (𝐵𝐹𝐶 → (𝐹𝐵) = 𝐶))
1716adantr 481 . 2 ((𝐹 Fn 𝐴𝐵𝐴) → (𝐵𝐹𝐶 → (𝐹𝐵) = 𝐶))
1813, 17impbid 202 1 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) = 𝐶𝐵𝐹𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1481  wcel 1988  ∃!weu 2468   class class class wbr 4644  Fun wfun 5870   Fn wfn 5871  cfv 5876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-iota 5839  df-fun 5878  df-fn 5879  df-fv 5884
This theorem is referenced by:  fnopfvb  6224  funbrfvb  6225  dffn5  6228  feqmptdf  6238  fnsnfv  6245  fndmdif  6307  dffo4  6361  dff13  6497  isomin  6572  isoini  6573  1stconst  7250  2ndconst  7251  fsplit  7267  seqomlem3  7532  seqomlem4  7533  nqerrel  9739  imasleval  16182  znleval  19884  axcontlem5  25829  elnlfn  28757  adjbd1o  28914  fcoinvbr  29391  elintfv  31638  br1steq  31646  br2ndeq  31647  fv1stcnv  31654  fv2ndcnv  31655  trpredpred  31702  scutun12  31891  madeval2  31910  fvbigcup  31984  fvsingle  32002  imageval  32012  brfullfun  32030  bj-mptval  33045  unccur  33363  poimirlem2  33382  poimirlem23  33403  pw2f1ocnv  37423  brcoffn  38148  funressnfv  40971  fnbrafvb  40997
  Copyright terms: Public domain W3C validator