Theorem cbvmpt2v 6901

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 4901, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.)

Hypotheses

Ref	Expression
cbvmpt2v.1	⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸)
cbvmpt2v.2	⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷)

Assertion

Ref	Expression
cbvmpt2v	⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷)

Distinct variable groups:   𝑥,𝑤,𝑦,𝑧,𝐴   𝑤,𝐵,𝑥,𝑦,𝑧   𝑤,𝐶,𝑧   𝑥,𝐷,𝑦

Allowed substitution hints:   𝐶(𝑥,𝑦)   𝐷(𝑧,𝑤)   𝐸(𝑥,𝑦,𝑧,𝑤)

Proof of Theorem cbvmpt2v

Step	Hyp	Ref	Expression
1		nfcv 2902	. 2 ⊢ Ⅎ𝑧𝐶
2		nfcv 2902	. 2 ⊢ Ⅎ𝑤𝐶
3		nfcv 2902	. 2 ⊢ Ⅎ𝑥𝐷
4		nfcv 2902	. 2 ⊢ Ⅎ𝑦𝐷
5		cbvmpt2v.1	. . 3 ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸)
6		cbvmpt2v.2	. . 3 ⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷)
7	5, 6	sylan9eq 2814	. 2 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷)
8	1, 2, 3, 4, 7	cbvmpt2 6900	1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷)

Syntax hints:   → wi 4   = wceq 1632   ↦ cmpt2 6816

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-opab 4865  df-oprab 6818  df-mpt2 6819

This theorem is referenced by:  seqomlem0  7714  dffi3  8504  cantnfsuc  8742  fin23lem33  9379  om2uzrdg  12969  uzrdgsuci  12973  sadcp1  15399  smupp1  15424  imasvscafn  16419  mgmnsgrpex  17639  sgrpnmndex  17640  sylow1  18238  sylow2b  18258  sylow3lem5  18266  sylow3  18268  efgmval  18345  efgtf  18355  frlmphl  20342  pmatcollpw3lem  20810  mp2pm2mplem3  20835  txbas  21592  bcth  23346  opnmbl  23590  mbfimaopn  23642  mbfi1fseq  23707  motplusg  25657  ttgval  25975  opsqrlem3  29331  mdetpmtr12  30221  madjusmdetlem4  30226  fvproj  30229  dya2iocival  30665  sxbrsigalem5  30680  sxbrsigalem6  30681  eulerpart  30774  sseqp1  30787  cvmliftlem15  31608  cvmlift2  31626  opnmbllem0  33776  mblfinlem1  33777  mblfinlem2  33778  sdc  33871  tendoplcbv  36583  dvhvaddcbv  36898  dvhvscacbv  36907  fsovcnvlem  38827  ntrneibex  38891  ioorrnopn  41046  hoidmvle  41338  ovnhoi  41341  hoimbl  41369  smflimlem6  41508  funcrngcsetc  42526  funcrngcsetcALT  42527  funcringcsetc  42563  lmod1zr  42810