Theorem cbvmpt2x 6375

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpt2 6376 allows to be a function of . (Contributed by NM, 29-Dec-2014.)

Hypotheses

Ref	Expression
cbvmpt2x.1
cbvmpt2x.2
cbvmpt2x.3
cbvmpt2x.4
cbvmpt2x.5
cbvmpt2x.6
cbvmpt2x.7
cbvmpt2x.8

Assertion

Ref	Expression
cbvmpt2x

Distinct variable groups:   ,,,,   ,   ,

Proof of Theorem cbvmpt2x

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1707	. . . . 5
2		cbvmpt2x.1	. . . . . 6
3	2	nfcri 2612	. . . . 5
4	1, 3	nfan 1928	. . . 4
5		cbvmpt2x.3	. . . . 5
6	5	nfeq2 2636	. . . 4
7	4, 6	nfan 1928	. . 3
8		nfv 1707	. . . . 5
9		nfcv 2619	. . . . . 6
10	9	nfcri 2612	. . . . 5
11	8, 10	nfan 1928	. . . 4
12		cbvmpt2x.4	. . . . 5
13	12	nfeq2 2636	. . . 4
14	11, 13	nfan 1928	. . 3
15		nfv 1707	. . . . 5
16		cbvmpt2x.2	. . . . . 6
17	16	nfcri 2612	. . . . 5
18	15, 17	nfan 1928	. . . 4
19		cbvmpt2x.5	. . . . 5
20	19	nfeq2 2636	. . . 4
21	18, 20	nfan 1928	. . 3
22		nfv 1707	. . . 4
23		cbvmpt2x.6	. . . . 5
24	23	nfeq2 2636	. . . 4
25	22, 24	nfan 1928	. . 3
26		eleq1 2529	. . . . . 6
27	26	adantr 465	. . . . 5
28		cbvmpt2x.7	. . . . . . 7
29	28	eleq2d 2527	. . . . . 6
30		eleq1 2529	. . . . . 6
31	29, 30	sylan9bb 699	. . . . 5
32	27, 31	anbi12d 710	. . . 4
33		cbvmpt2x.8	. . . . 5
34	33	eqeq2d 2471	. . . 4
35	32, 34	anbi12d 710	. . 3
36	7, 14, 21, 25, 35	cbvoprab12 6371	. 2
37		df-mpt2 6301	. 2
38		df-mpt2 6301	. 2
39	36, 37, 38	3eqtr4i 2496	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  F/_wnfc 2605  {coprab 6297  e.cmpt2 6298

This theorem is referenced by:  cbvmpt2  6376  mpt2mptsx  6863  dmmpt2ssx  6865  gsumcom2  17003  ptcmpg  20557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-opab 4511  df-oprab 6300  df-mpt2 6301