Theorem cbvmpov 7453

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

Hypotheses

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

Assertion

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

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

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

Proof of Theorem cbvmpov

Dummy variable 𝑣 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1w 2820	. . . . 5 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))
2		eleq1w 2820	. . . . 5 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵))
3	1, 2	bi2anan9 639	. . . 4 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)))
4		cbvmpov.1	. . . . . 6 ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸)
5		cbvmpov.2	. . . . . 6 ⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷)
6	4, 5	sylan9eq 2792	. . . . 5 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷)
7	6	eqeq2d 2748	. . . 4 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑣 = 𝐶 ↔ 𝑣 = 𝐷))
8	3, 7	anbi12d 633	. . 3 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 = 𝐷)))
9	8	cbvoprab12v 7448	. 2 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑣⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶)} = {⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∣ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 = 𝐷)}
10		df-mpo 7363	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑣⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶)}
11		df-mpo 7363	. 2 ⊢ (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∣ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 = 𝐷)}
12	9, 10, 11	3eqtr4i 2770	1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {coprab 7359   ∈ cmpo 7360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-oprab 7362  df-mpo 7363

This theorem is referenced by:  fvproj  8075  seqomlem0  8379  dffi3  9335  cantnfsuc  9580  fin23lem33  10256  om2uzrdg  13880  uzrdgsuci  13884  sadcp1  16383  smupp1  16408  imasvscafn  17459  mgmnsgrpex  18860  sgrpnmndex  18861  sylow1  19536  sylow2b  19556  sylow3lem5  19564  sylow3  19566  efgmval  19645  efgtf  19655  funcrngcsetc  20575  funcrngcsetcALT  20576  funcringcsetc  20609  frlmphl  21738  pmatcollpw3lem  22726  mp2pm2mplem3  22751  txbas  23510  mpomulcn  24812  bcth  25274  opnmbl  25547  mbfimaopn  25601  mbfi1fseq  25666  om2noseqrdg  28284  noseqrdgsuc  28288  motplusg  28598  ttgval  28931  opsqrlem3  32202  elrgspnlem2  33309  splysubrg  33709  issply  33710  fedgmul  33781  mdetpmtr12  33975  madjusmdetlem4  33980  dya2iocival  34423  sxbrsigalem5  34438  sxbrsigalem6  34439  eulerpart  34532  sseqp1  34545  cvmliftlem15  35486  cvmlift2  35504  opnmbllem0  37968  mblfinlem1  37969  mblfinlem2  37970  sdc  38056  tendoplcbv  41212  dvhvaddcbv  41526  dvhvscacbv  41535  fsovcnvlem  44443  ntrneibex  44503  ioorrnopn  46737  hoidmvle  47032  ovnhoi  47035  hoimbl  47063  smflimlem6  47208  lmod1zr  48927  functhinclem4  49880