Theorem fniniseg 6453

Description: Membership in the preimage of a singleton, under a function. (Contributed by Mario Carneiro, 12-May-2014.) (Proof shortened by Mario Carneiro , 28-Apr-2015.)

Assertion

Ref	Expression
fniniseg	⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)))

Proof of Theorem fniniseg

Step	Hyp	Ref	Expression
1		elpreima 6452	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵})))
2		fvex 6314	. . . 4 ⊢ (𝐹‘𝐶) ∈ V
3	2	elsn 4300	. . 3 ⊢ ((𝐹‘𝐶) ∈ {𝐵} ↔ (𝐹‘𝐶) = 𝐵)
4	3	anbi2i 732	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))
5	1, 4	syl6bb 276	1 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1596   ∈ wcel 2103  {csn 4285  ^◡ccnv 5217   “ cima 5221   Fn wfn 5996  ‘cfv 6001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pr 5011

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-sbc 3542  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-br 4761  df-opab 4821  df-id 5128  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-iota 5964  df-fun 6003  df-fn 6004  df-fv 6009

This theorem is referenced by:  fparlem1  7397  fparlem2  7398  pw2f1olem  8180  recmulnq  9899  dmrecnq  9903  vdwlem1  15808  vdwlem2  15809  vdwlem6  15813  vdwlem8  15815  vdwlem9  15816  vdwlem12  15819  vdwlem13  15820  ramval  15835  ramub1lem1  15853  ghmeqker  17809  efgrelexlemb  18284  efgredeu  18286  psgnevpmb  20056  qtopeu  21642  itg1addlem1  23579  i1faddlem  23580  i1fmullem  23581  i1fmulclem  23589  i1fres  23592  itg10a  23597  itg1ge0a  23598  itg1climres  23601  mbfi1fseqlem4  23605  ply1remlem  24042  ply1rem  24043  fta1glem1  24045  fta1glem2  24046  fta1g  24047  fta1blem  24048  plyco0  24068  ofmulrt  24157  plyremlem  24179  plyrem  24180  fta1lem  24182  fta1  24183  vieta1lem1  24185  vieta1lem2  24186  vieta1  24187  plyexmo  24188  elaa  24191  aannenlem1  24203  aalioulem2  24208  pilem1  24325  efif1olem3  24410  efif1olem4  24411  efifo  24413  eff1olem  24414  basellem4  24930  lgsqrlem2  25192  lgsqrlem3  25193  rpvmasum2  25321  dirith  25338  foresf1o  29571  ofpreima  29695  1stpreimas  29713  locfinreflem  30137  qqhre  30294  indpi1  30312  indpreima  30317  sibfof  30632  cvmliftlem6  31500  cvmliftlem7  31501  cvmliftlem8  31502  cvmliftlem9  31503  taupilem3  33397  itg2addnclem  33693  itg2addnclem2  33694  pw2f1o2val2  38026  dnnumch3  38036  proot1mul  38196  proot1hash  38197  proot1ex  38198  wessf1ornlem  39787