Theorem funbrfv2b 6909

Description: Function value in terms of a binary relation. (Contributed by Mario Carneiro, 19-Mar-2014.)

Assertion

Ref	Expression
funbrfv2b	⊢ (Fun 𝐹 → (𝐴𝐹𝐵 ↔ (𝐴 ∈ dom 𝐹 ∧ (𝐹‘𝐴) = 𝐵)))

Proof of Theorem funbrfv2b

Step	Hyp	Ref	Expression
1		funrel 6523	. . . 4 ⊢ (Fun 𝐹 → Rel 𝐹)
2		releldm 5909	. . . . 5 ⊢ ((Rel 𝐹 ∧ 𝐴𝐹𝐵) → 𝐴 ∈ dom 𝐹)
3	2	ex 415	. . . 4 ⊢ (Rel 𝐹 → (𝐴𝐹𝐵 → 𝐴 ∈ dom 𝐹))
4	1, 3	syl 17	. . 3 ⊢ (Fun 𝐹 → (𝐴𝐹𝐵 → 𝐴 ∈ dom 𝐹))
5	4	pm4.71rd 569	. 2 ⊢ (Fun 𝐹 → (𝐴𝐹𝐵 ↔ (𝐴 ∈ dom 𝐹 ∧ 𝐴𝐹𝐵)))
6		funbrfvb 6905	. . 3 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) = 𝐵 ↔ 𝐴𝐹𝐵))
7	6	pm5.32da 586	. 2 ⊢ (Fun 𝐹 → ((𝐴 ∈ dom 𝐹 ∧ (𝐹‘𝐴) = 𝐵) ↔ (𝐴 ∈ dom 𝐹 ∧ 𝐴𝐹𝐵)))
8	5, 7	bitr4d 284	1 ⊢ (Fun 𝐹 → (𝐴𝐹𝐵 ↔ (𝐴 ∈ dom 𝐹 ∧ (𝐹‘𝐴) = 𝐵)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1550   ∈ wcel 2132   class class class wbr 5090  dom cdm 5636  Rel wrel 5641  Fun wfun 6500  ‘cfv 6506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pr 5380

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-ne 2948  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-id 5531  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-iota 6462  df-fun 6508  df-fn 6509  df-fv 6514

This theorem is referenced by:  funcnvmpt  6962  brtpos2  8196  mpocurryd  8233  xpcomco  9024  fseqenlem2  9967  fpwwe2  10587  joinfval  18375  joinfval2  18376  meetfval  18389  meetfval2  18390  tayl0  26391  ofpreima  32806  curf  38035  uncf  38036  curunc  38039  fperdvper  46431