Theorem fnbrfvb 6711

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.

Step	Hyp	Ref	Expression
1		eqid 2819	. . . 4 ⊢ (𝐹‘𝐵) = (𝐹‘𝐵)
2		fvex 6676	. . . . 5 ⊢ (𝐹‘𝐵) ∈ V
3		eqeq2 2831	. . . . . . 7 ⊢ (𝑥 = (𝐹‘𝐵) → ((𝐹‘𝐵) = 𝑥 ↔ (𝐹‘𝐵) = (𝐹‘𝐵)))
4		breq2 5061	. . . . . . 7 ⊢ (𝑥 = (𝐹‘𝐵) → (𝐵𝐹𝑥 ↔ 𝐵𝐹(𝐹‘𝐵)))
5	3, 4	bibi12d 348	. . . . . 6 ⊢ (𝑥 = (𝐹‘𝐵) → (((𝐹‘𝐵) = 𝑥 ↔ 𝐵𝐹𝑥) ↔ ((𝐹‘𝐵) = (𝐹‘𝐵) ↔ 𝐵𝐹(𝐹‘𝐵))))
6	5	imbi2d 343	. . . . 5 ⊢ (𝑥 = (𝐹‘𝐵) → (((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = 𝑥 ↔ 𝐵𝐹𝑥)) ↔ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = (𝐹‘𝐵) ↔ 𝐵𝐹(𝐹‘𝐵)))))
7		fneu 6454	. . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ∃!𝑥 𝐵𝐹𝑥)
8		tz6.12c 6688	. . . . . 6 ⊢ (∃!𝑥 𝐵𝐹𝑥 → ((𝐹‘𝐵) = 𝑥 ↔ 𝐵𝐹𝑥))
9	7, 8	syl 17	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = 𝑥 ↔ 𝐵𝐹𝑥))
10	2, 6, 9	vtocl 3558	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = (𝐹‘𝐵) ↔ 𝐵𝐹(𝐹‘𝐵)))
11	1, 10	mpbii 235	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵𝐹(𝐹‘𝐵))
12		breq2 5061	. . 3 ⊢ ((𝐹‘𝐵) = 𝐶 → (𝐵𝐹(𝐹‘𝐵) ↔ 𝐵𝐹𝐶))
13	11, 12	syl5ibcom 247	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = 𝐶 → 𝐵𝐹𝐶))
14		fnfun 6446	. . . 4 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
15		funbrfv 6709	. . . 4 ⊢ (Fun 𝐹 → (𝐵𝐹𝐶 → (𝐹‘𝐵) = 𝐶))
16	14, 15	syl 17	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵𝐹𝐶 → (𝐹‘𝐵) = 𝐶))
17	16	adantr 483	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐵𝐹𝐶 → (𝐹‘𝐵) = 𝐶))
18	13, 17	impbid 214	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = 𝐶 ↔ 𝐵𝐹𝐶))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1531   ∈ wcel 2108  ∃!weu 2647   class class class wbr 5057  Fun wfun 6342   Fn wfn 6343  ‘cfv 6348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-iota 6307  df-fun 6350  df-fn 6351  df-fv 6356

This theorem is referenced by:  fnopfvb  6712  funbrfvb  6713  fnbrfvb2  6715  dffn5  6717  feqmptdf  6728  fnsnfv  6736  fndmdif  6805  dffo4  6862  dff13  7005  isomin  7082  isoini  7083  br1steqg  7703  br2ndeqg  7704  1stconst  7787  2ndconst  7788  fsplit  7804  fsplitOLD  7805  seqomlem3  8080  seqomlem4  8081  nqerrel  10346  imasleval  16806  znleval  20693  axcontlem5  26746  elnlfn  29697  adjbd1o  29854  fcoinvbr  30350  fv1stcnv  33013  fv2ndcnv  33014  trpredpred  33060  scutun12  33264  madeval2  33283  fvbigcup  33356  fvsingle  33374  imageval  33384  brfullfun  33402  bj-mptval  34401  unccur  34867  poimirlem2  34886  poimirlem23  34907  pw2f1ocnv  39624  brcoffn  40370  funressnfv  43268  fnbrafvb  43343