Theorem fniniseg 7057

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 7055	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵})))
2		fvex 6896	. . . 4 ⊢ (𝐹‘𝐶) ∈ V
3	2	elsn 4599	. . 3 ⊢ ((𝐹‘𝐶) ∈ {𝐵} ↔ (𝐹‘𝐶) = 𝐵)
4	3	anbi2i 635	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))
5	1, 4	bitrdi 290	1 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {csn 4584  ^◡ccnv 5650   “ cima 5654   Fn wfn 6532  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-fv 6545

This theorem is used by:  fparlem1  8121  fparlem2  8122  pw2f1olem  9093  recmulnq  11042  dmrecnq  11046  indpi1  12327  vdwlem1  17152  vdwlem2  17153  vdwlem6  17157  vdwlem8  17159  vdwlem9  17160  vdwlem12  17163  vdwlem13  17164  ramval  17179  ramub1lem1  17197  ghmeqker  19450  ghmqusnsglem1  19487  ghmquskerlem1  19490  ghmqusker  19494  efgrelexlemb  19957  efgredeu  19959  psgnevpmb  21886  qtopeu  24028  itg1addlem1  26006  i1faddlem  26007  i1fmullem  26008  i1fmulclem  26016  i1fres  26019  itg10a  26024  itg1ge0a  26025  itg1climres  26028  mbfi1fseqlem4  26032  ply1remlem  26476  ply1rem  26477  fta1glem1  26479  fta1glem2  26480  fta1g  26481  fta1blem  26482  plyco0  26503  ofmulrt  26593  plyremlem  26618  plyrem  26619  fta1lem  26621  fta1  26622  rnplynfin  26623  plyconz  26624  vieta1lem1  26626  vieta1lem2  26627  vieta1  26628  plyexmo  26629  elaa  26632  aannenlem1  26648  aalioulem2  26653  pilem1  26771  efif1olem3  26865  efif1olem4  26866  efifo  26868  eff1olem  26869  basellem4  27404  lgsqrlem2  27667  lgsqrlem3  27668  rpvmasum2  27832  dirith  27849  foresf1o  33093  ofpreima  33252  fnpreimac  33257  1stpreimas  33292  indpreima  33425  s3clhash  33505  pwrssmgc  33554  cycpmconjslem2  33709  cyc3conja  33711  exsslsb  34222  dimkerim  34252  elirng  34311  irngss  34312  irngnzply1  34316  locfinreflem  34465  qqhre  34645  sibfof  34965  cvmliftlem6  36034  cvmliftlem7  36035  cvmliftlem8  36036  cvmliftlem9  36037  taupilem3  38220  itg2addnclem  38569  itg2addnclem2  38570  pw2f1o2val2  44026  dnnumch3  44033  proot1mul  44180  proot1hash  44181  proot1ex  44182  wessf1ornlem  46169  preimafvsnel  48430  uniimaprimaeqfv  48433  elsetpreimafvbi  48442  imasubc  50228  imassc  50230  imaid  50231