Theorem funopfv 5969

Description: The second element in an ordered pair member of a function is the function's value. (Contributed by NM, 19-Jul-1996.)

Assertion

Ref	Expression
funopfv	⊢ (Fun 𝐹 → (⟨𝐴, 𝐵⟩ ∈ 𝐹 → (𝐹‘𝐴) = 𝐵))

Proof of Theorem funopfv

Step	Hyp	Ref	Expression
1		df-br 4435	. 2 ⊢ (𝐴𝐹𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝐹)
2		funbrfv 5968	. 2 ⊢ (Fun 𝐹 → (𝐴𝐹𝐵 → (𝐹‘𝐴) = 𝐵))
3	1, 2	syl5bir 228	1 ⊢ (Fun 𝐹 → (⟨𝐴, 𝐵⟩ ∈ 𝐹 → (𝐹‘𝐴) = 𝐵))

Syntax hints:   → wi 4   = wceq 1468   ∈ wcel 1937  ⟨cop 4001   class class class wbr 4434  Fun wfun 5627  ‘cfv 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pr 4680

This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3068  df-sbc 3292  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002  df-uni 4229  df-br 4435  df-opab 4494  df-id 4795  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-iota 5597  df-fun 5635  df-fv 5641

This theorem is referenced by:  fvopab3ig  6012  fvsn  6165  fveqf1o  6271  ovidig  6489  ovigg  6492  f1o2ndf1  6983  fundmen  7727  uzrdg0i  12286  uzrdgsuci  12287  strfvd  15319  strfv2d  15320  imasaddvallem  15600  imasvscafn  15608  adjeq  27751  bnj1379  29794  bnj97  29829  bnj553  29861  bnj966  29907  bnj1442  30010  basvtxval  39649  edgfiedgval  39650