Theorem cbvmpt2v 6900

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 6899	1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷)

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

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 6817  df-mpt2 6818

This theorem is referenced by:  seqomlem0  7713  dffi3  8502  cantnfsuc  8740  fin23lem33  9359  om2uzrdg  12949  uzrdgsuci  12953  sadcp1  15379  smupp1  15404  imasvscafn  16399  mgmnsgrpex  17619  sgrpnmndex  17620  sylow1  18218  sylow2b  18238  sylow3lem5  18246  sylow3  18248  efgmval  18325  efgtf  18335  frlmphl  20322  pmatcollpw3lem  20790  mp2pm2mplem3  20815  txbas  21572  bcth  23326  opnmbl  23570  mbfimaopn  23622  mbfi1fseq  23687  motplusg  25636  ttgval  25954  opsqrlem3  29310  mdetpmtr12  30200  madjusmdetlem4  30205  fvproj  30208  dya2iocival  30644  sxbrsigalem5  30659  sxbrsigalem6  30660  eulerpart  30753  sseqp1  30766  cvmliftlem15  31587  cvmlift2  31605  opnmbllem0  33758  mblfinlem1  33759  mblfinlem2  33760  sdc  33853  tendoplcbv  36565  dvhvaddcbv  36880  dvhvscacbv  36889  fsovcnvlem  38809  ntrneibex  38873  ioorrnopn  41028  hoidmvle  41320  ovnhoi  41323  hoimbl  41351  smflimlem6  41490  funcrngcsetc  42508  funcrngcsetcALT  42509  funcringcsetc  42545  lmod1zr  42792