MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbviin Structured version   Visualization version   GIF version

Theorem cbviin 4524
Description: Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009.) (Revised by Mario Carneiro, 14-Oct-2016.)
Hypotheses
Ref Expression
cbviun.1 𝑦𝐵
cbviun.2 𝑥𝐶
cbviun.3 (𝑥 = 𝑦𝐵 = 𝐶)
Assertion
Ref Expression
cbviin 𝑥𝐴 𝐵 = 𝑦𝐴 𝐶
Distinct variable groups:   𝑦,𝐴   𝑥,𝐴
Allowed substitution hints:   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)

Proof of Theorem cbviin
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 cbviun.1 . . . . 5 𝑦𝐵
21nfcri 2755 . . . 4 𝑦 𝑧𝐵
3 cbviun.2 . . . . 5 𝑥𝐶
43nfcri 2755 . . . 4 𝑥 𝑧𝐶
5 cbviun.3 . . . . 5 (𝑥 = 𝑦𝐵 = 𝐶)
65eleq2d 2684 . . . 4 (𝑥 = 𝑦 → (𝑧𝐵𝑧𝐶))
72, 4, 6cbvral 3155 . . 3 (∀𝑥𝐴 𝑧𝐵 ↔ ∀𝑦𝐴 𝑧𝐶)
87abbii 2736 . 2 {𝑧 ∣ ∀𝑥𝐴 𝑧𝐵} = {𝑧 ∣ ∀𝑦𝐴 𝑧𝐶}
9 df-iin 4488 . 2 𝑥𝐴 𝐵 = {𝑧 ∣ ∀𝑥𝐴 𝑧𝐵}
10 df-iin 4488 . 2 𝑦𝐴 𝐶 = {𝑧 ∣ ∀𝑦𝐴 𝑧𝐶}
118, 9, 103eqtr4i 2653 1 𝑥𝐴 𝐵 = 𝑦𝐴 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wcel 1987  {cab 2607  wnfc 2748  wral 2907   ciin 4486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-iin 4488
This theorem is referenced by:  cbviinv  4526  elrfirn2  36736  fnlimfvre  39307  smflimlem6  40288  smflim  40289  smflim2  40316  smfsup  40324  smfinflem  40327  smfinf  40328  smflimsup  40338
  Copyright terms: Public domain W3C validator