Theorem funimass4 6973

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Raph Levien, 20-Nov-2006.)

Assertion

Ref	Expression
funimass4	⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

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

Proof of Theorem funimass4

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ss 3980	. . 3 ⊢ ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ ∀𝑦(𝑦 ∈ (𝐹 “ 𝐴) → 𝑦 ∈ 𝐵))
2		vex 3482	. . . . . . . . 9 ⊢ 𝑦 ∈ V
3	2	elima 6085	. . . . . . . 8 ⊢ (𝑦 ∈ (𝐹 “ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦)
4		eqcom 2742	. . . . . . . . . 10 ⊢ (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝑦)
5		ssel 3989	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ dom 𝐹 → (𝑥 ∈ 𝐴 → 𝑥 ∈ dom 𝐹))
6		funbrfvb 6962	. . . . . . . . . . . . 13 ⊢ ((Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦))
7	6	ex 412	. . . . . . . . . . . 12 ⊢ (Fun 𝐹 → (𝑥 ∈ dom 𝐹 → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦)))
8	5, 7	syl9 77	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ dom 𝐹 → (Fun 𝐹 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦))))
9	8	imp31 417	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹) ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦))
10	4, 9	bitrid 283	. . . . . . . . 9 ⊢ (((𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹) ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑦))
11	10	rexbidva 3175	. . . . . . . 8 ⊢ ((𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹) → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦))
12	3, 11	bitr4id 290	. . . . . . 7 ⊢ ((𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹) → (𝑦 ∈ (𝐹 “ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)))
13	12	imbi1d 341	. . . . . 6 ⊢ ((𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹) → ((𝑦 ∈ (𝐹 “ 𝐴) → 𝑦 ∈ 𝐵) ↔ (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵)))
14		r19.23v 3181	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵) ↔ (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵))
15	13, 14	bitr4di 289	. . . . 5 ⊢ ((𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹) → ((𝑦 ∈ (𝐹 “ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵)))
16	15	albidv 1918	. . . 4 ⊢ ((𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹) → (∀𝑦(𝑦 ∈ (𝐹 “ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵)))
17		ralcom4 3284	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵))
18		fvex 6920	. . . . . . 7 ⊢ (𝐹‘𝑥) ∈ V
19		eleq1 2827	. . . . . . 7 ⊢ (𝑦 = (𝐹‘𝑥) → (𝑦 ∈ 𝐵 ↔ (𝐹‘𝑥) ∈ 𝐵))
20	18, 19	ceqsalv 3519	. . . . . 6 ⊢ (∀𝑦(𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵) ↔ (𝐹‘𝑥) ∈ 𝐵)
21	20	ralbii 3091	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
22	17, 21	bitr3i 277	. . . 4 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
23	16, 22	bitrdi 287	. . 3 ⊢ ((𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹) → (∀𝑦(𝑦 ∈ (𝐹 “ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
24	1, 23	bitrid 283	. 2 ⊢ ((𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹) → ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
25	24	ancoms 458	1 ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1535   = wceq 1537   ∈ wcel 2106  ∀wral 3059  ∃wrex 3068   ⊆ wss 3963   class class class wbr 5148  dom cdm 5689   “ cima 5692  Fun wfun 6557  ‘cfv 6563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-fv 6571

This theorem is referenced by:  funimass3  7074  funimass5  7075  funconstss  7076  fssrescdmd  7146  funimassov  7610  fnwelem  8155  cnfcomlem  9737  dfac12lem2  10183  ackbij1b  10276  wunom  10758  phimullem  16813  frmdss2  18889  cntzmhm2  19373  dprd2da  20077  frlmsslsp  21834  1stckgenlem  23577  txcnp  23644  ptcnplem  23645  xkopt  23679  xkoinjcn  23711  tgqtop  23736  uzrest  23921  cnflf2  24027  lmflf  24029  txflf  24030  cnextcn  24091  ghmcnp  24139  ucnima  24306  metcnp  24570  tcphcph  25285  ovolficcss  25518  opnmbllem  25650  ellimc2  25927  ellimc3  25929  deg1n0ima  26143  dvloglem  26705  logf1o2  26707  dchrghm  27315  madebdayim  27941  madefi  27965  oldfi  27966  addsbdaylem  28064  negsproplem2  28076  negsbdaylem  28103  upgrreslem  29336  umgrreslem  29337  xrofsup  32778  eulerpartlemd  34348  erdszelem2  35177  cvmlift3lem7  35310  mclsax  35554  filnetlem4  36364  poimir  37640  opnmbllem0  37643  cnres2  37750  icccncfext  45843  isubgruhgr  47792