Theorem foelrn 7094

Description: Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.)

Assertion

Ref	Expression
foelrn	⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝐶 = (𝐹‘𝑥))

Distinct variable groups:   𝑥,𝐹   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶

Proof of Theorem foelrn

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dffo3 7089	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)))
2	1	simprbi 496	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))
3		eqeq1 2738	. . . 4 ⊢ (𝑦 = 𝐶 → (𝑦 = (𝐹‘𝑥) ↔ 𝐶 = (𝐹‘𝑥)))
4	3	rexbidv 3162	. . 3 ⊢ (𝑦 = 𝐶 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 𝐶 = (𝐹‘𝑥)))
5	4	rspccva 3598	. 2 ⊢ ((∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ∧ 𝐶 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝐶 = (𝐹‘𝑥))
6	2, 5	sylan 580	1 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝐶 = (𝐹‘𝑥))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ∀wral 3050  ∃wrex 3059  ⟶wf 6524  –onto→wfo 6526  ‘cfv 6528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5264  ax-nul 5274  ax-pr 5400

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4882  df-br 5118  df-opab 5180  df-mpt 5200  df-id 5546  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-iota 6481  df-fun 6530  df-fn 6531  df-f 6532  df-fo 6534  df-fv 6536

This theorem is referenced by:  foco2  7096  fofinf1o  9339  fodomacn  10063  iunfictbso  10121  cff1  10265  cofsmo  10276  axcclem  10464  konigthlem  10575  tskuni  10790  fulli  17915  efgredlemc  19713  efgrelexlemb  19718  efgredeu  19720  ghmcyg  19864  znfld  21508  znrrg  21513  cygznlem3  21517  ovoliunnul  25447  lgsdchr  27304  foresf1o  32419  iunrdx  32478  znfermltl  33318  crngohomfo  37959  fourierdlem20  46092  fourierdlem52  46123  fourierdlem63  46134  fourierdlem64  46135  fourierdlem65  46136  isuspgrimlem  47827  grimedg  47856