Theorem elrnmpt1 5950

Description: Elementhood in an image set. (Contributed by Mario Carneiro, 31-Aug-2015.)

Hypothesis

Ref	Expression
rnmpt.1	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)

Assertion

Ref	Expression
elrnmpt1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ ran 𝐹)

Proof of Theorem elrnmpt1

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3459	. . . 4 ⊢ 𝑥 ∈ V
2		id 23	. . . . . . 7 ⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧)
3		csbeq1a 3867	. . . . . . 7 ⊢ (𝑥 = 𝑧 → 𝐴 = ⦋𝑧 / 𝑥⦌𝐴)
4	2, 3	eleq12d 2857	. . . . . 6 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴))
5		csbeq1a 3867	. . . . . . 7 ⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵)
6	5	biantrud 540	. . . . . 6 ⊢ (𝑥 = 𝑧 → (𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ↔ (𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝐵 = ⦋𝑧 / 𝑥⦌𝐵)))
7	4, 6	bitr2d 283	. . . . 5 ⊢ (𝑥 = 𝑧 → ((𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) ↔ 𝑥 ∈ 𝐴))
8	7	equcoms 2050	. . . 4 ⊢ (𝑧 = 𝑥 → ((𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) ↔ 𝑥 ∈ 𝐴))
9	1, 8	spcev 3565	. . 3 ⊢ (𝑥 ∈ 𝐴 → ∃𝑧(𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝐵 = ⦋𝑧 / 𝑥⦌𝐵))
10		df-rex 3090	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
11		nfv 1944	. . . . . . 7 ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
12		nfcsb1v 3877	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐴
13	12	nfcri 2917	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴
14		nfcsb1v 3877	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵
15	14	nfeq2 2942	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑦 = ⦋𝑧 / 𝑥⦌𝐵
16	13, 15	nfan 1929	. . . . . . 7 ⊢ Ⅎ𝑥(𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝑦 = ⦋𝑧 / 𝑥⦌𝐵)
17	5	eqeq2d 2774	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑦 = 𝐵 ↔ 𝑦 = ⦋𝑧 / 𝑥⦌𝐵))
18	4, 17	anbi12d 643	. . . . . . 7 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝑦 = ⦋𝑧 / 𝑥⦌𝐵)))
19	11, 16, 18	cbvexv1 2374	. . . . . 6 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ ∃𝑧(𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝑦 = ⦋𝑧 / 𝑥⦌𝐵))
20	10, 19	bitri 278	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑧(𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝑦 = ⦋𝑧 / 𝑥⦌𝐵))
21		eqeq1 2767	. . . . . . 7 ⊢ (𝑦 = 𝐵 → (𝑦 = ⦋𝑧 / 𝑥⦌𝐵 ↔ 𝐵 = ⦋𝑧 / 𝑥⦌𝐵))
22	21	anbi2d 641	. . . . . 6 ⊢ (𝑦 = 𝐵 → ((𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝑦 = ⦋𝑧 / 𝑥⦌𝐵) ↔ (𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝐵 = ⦋𝑧 / 𝑥⦌𝐵)))
23	22	exbidv 1951	. . . . 5 ⊢ (𝑦 = 𝐵 → (∃𝑧(𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝑦 = ⦋𝑧 / 𝑥⦌𝐵) ↔ ∃𝑧(𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝐵 = ⦋𝑧 / 𝑥⦌𝐵)))
24	20, 23	bitrid 286	. . . 4 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑧(𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝐵 = ⦋𝑧 / 𝑥⦌𝐵)))
25		rnmpt.1	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
26	25	rnmpt 5947	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}
27	24, 26	elab2g 3639	. . 3 ⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑧(𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝐵 = ⦋𝑧 / 𝑥⦌𝐵)))
28	9, 27	imbitrrid 249	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝑥 ∈ 𝐴 → 𝐵 ∈ ran 𝐹))
29	28	impcom 412	1 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ ran 𝐹)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570  ∃wex 1809   ∈ wcel 2143  ∃wrex 3089  ⦋csb 3853   ↦ cmpt 5192  ran crn 5662

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-pr 5404

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-mpt 5193  df-cnv 5669  df-dm 5671  df-rn 5672

This theorem is used by:  elrnmpt1d  5954  fliftel1  7308  minveclem4  25600  minvecolem4  31241  rexunirn  32847  esum2d  34492  exrecfnlem  38053  totbndbnd  38468  rrnequiv  38514  suprnmpt  45920  disjf1o  45937  disjinfi  45938  choicefi  45945  suprubrnmpt  45996  supxrleubrnmpt  46148  suprleubrnmpt  46164  infrnmptle  46165  infxrunb3rnmpt  46170  supminfrnmpt  46187  infxrgelbrnmpt  46196  fourierdlem31  46880  ioorrnopnlem  47046  sge0supre  47131  sge0gerp  47137  sge0iunmpt  47160  sge0rernmpt  47164  sge0reuz  47189  meadjiunlem  47207  iunhoiioolem  47417  vonioolem1  47422  smfpimcclem  47549