Theorem funbrfv 6883

Description: The second argument of a binary relation on a function is the function's value. (Contributed by NM, 30-Apr-2004.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
funbrfv	⊢ (Fun 𝐹 → (𝐴𝐹𝐵 → (𝐹‘𝐴) = 𝐵))

Proof of Theorem funbrfv

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		funrel 6510	. . . 4 ⊢ (Fun 𝐹 → Rel 𝐹)
2		brrelex2 5679	. . . 4 ⊢ ((Rel 𝐹 ∧ 𝐴𝐹𝐵) → 𝐵 ∈ V)
3	1, 2	sylan 581	. . 3 ⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → 𝐵 ∈ V)
4		breq2 5090	. . . . . 6 ⊢ (𝑦 = 𝐵 → (𝐴𝐹𝑦 ↔ 𝐴𝐹𝐵))
5	4	anbi2d 631	. . . . 5 ⊢ (𝑦 = 𝐵 → ((Fun 𝐹 ∧ 𝐴𝐹𝑦) ↔ (Fun 𝐹 ∧ 𝐴𝐹𝐵)))
6		eqeq2 2749	. . . . 5 ⊢ (𝑦 = 𝐵 → ((𝐹‘𝐴) = 𝑦 ↔ (𝐹‘𝐴) = 𝐵))
7	5, 6	imbi12d 344	. . . 4 ⊢ (𝑦 = 𝐵 → (((Fun 𝐹 ∧ 𝐴𝐹𝑦) → (𝐹‘𝐴) = 𝑦) ↔ ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → (𝐹‘𝐴) = 𝐵)))
8		funeu 6518	. . . . . 6 ⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝑦) → ∃!𝑦 𝐴𝐹𝑦)
9		tz6.12-1 6858	. . . . . 6 ⊢ ((𝐴𝐹𝑦 ∧ ∃!𝑦 𝐴𝐹𝑦) → (𝐹‘𝐴) = 𝑦)
10	8, 9	sylan2 594	. . . . 5 ⊢ ((𝐴𝐹𝑦 ∧ (Fun 𝐹 ∧ 𝐴𝐹𝑦)) → (𝐹‘𝐴) = 𝑦)
11	10	anabss7 674	. . . 4 ⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝑦) → (𝐹‘𝐴) = 𝑦)
12	7, 11	vtoclg 3500	. . 3 ⊢ (𝐵 ∈ V → ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → (𝐹‘𝐴) = 𝐵))
13	3, 12	mpcom 38	. 2 ⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → (𝐹‘𝐴) = 𝐵)
14	13	ex 412	1 ⊢ (Fun 𝐹 → (𝐴𝐹𝐵 → (𝐹‘𝐴) = 𝐵))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃!weu 2569  Vcvv 3430   class class class wbr 5086  Rel wrel 5630  Fun wfun 6487  ‘cfv 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6449  df-fun 6495  df-fv 6501

This theorem is referenced by:  funopfv  6884  fnbrfvb  6885  fvelima2  6887  fvelima  6900  fvelimad  6902  fvi  6911  opabiota  6917  fmptco  7077  fliftfun  7261  fliftval  7265  tfrlem5  8313  fpwwe2  10560  nqerid  10850  sum0  15677  sumz  15678  fsumsers  15684  isumclim  15713  ntrivcvgfvn0  15858  ntrivcvgtail  15859  zprodn0  15898  iprodclim  15957  idinv  17750  cnextfvval  24043  cnextfres  24047  dvadd  25920  dvmul  25921  dvco  25927  dvcj  25930  dvrec  25935  dvcnv  25957  dvef  25960  ftc1cn  26023  ulmdv  26384  minvecolem4b  30967  minvecolem4  30969  hlimuni  31327  chscllem4  31729  fmptcof2  32748  fvtransport  36233  fvray  36342  fvline  36345  ftc1cnnc  38030  iscard4  43981  frege124d  44209