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

Theorem cbvabv 2869
Description: Rule used to change bound variables, using implicit substitution. Version of cbvab 2872 with disjoint variable conditions requiring fewer axioms. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2159 and ax-13 2382. (Revised by Steven Nguyen, 4-Dec-2022.)
Hypothesis
Ref Expression
cbvabv.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvabv {𝑥𝜑} = {𝑦𝜓}
Distinct variable groups:   𝜑,𝑦   𝜓,𝑥   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvabv
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 sbco2vv 2106 . . . 4 ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑)
2 cbvabv.1 . . . . . 6 (𝑥 = 𝑦 → (𝜑𝜓))
32sbievw 2101 . . . . 5 ([𝑦 / 𝑥]𝜑𝜓)
43sbbii 2081 . . . 4 ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
51, 4bitr3i 280 . . 3 ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
6 df-clab 2780 . . 3 (𝑧 ∈ {𝑥𝜑} ↔ [𝑧 / 𝑥]𝜑)
7 df-clab 2780 . . 3 (𝑧 ∈ {𝑦𝜓} ↔ [𝑧 / 𝑦]𝜓)
85, 6, 73bitr4i 306 . 2 (𝑧 ∈ {𝑥𝜑} ↔ 𝑧 ∈ {𝑦𝜓})
98eqriv 2798 1 {𝑥𝜑} = {𝑦𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  [wsb 2069  wcel 2112  {cab 2779
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 1911  ax-6 1970  ax-7 2015  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794
This theorem is referenced by:  cbvrabv  3442  difjust  3886  unjust  3888  injust  3890  uniiunlem  4015  dfif3  4442  pwjust  4501  snjust  4527  intab  4871  intabs  5212  iotajust  6286  wfrlem1  7941  sbth  8625  cardprc  9397  iunfictbso  9529  aceq3lem  9535  isf33lem  9781  axdc3  9869  axdclem  9934  axdc  9936  genpv  10414  ltexpri  10458  recexpr  10466  supsr  10527  hashf1lem2  13814  cvbtrcl  14347  mertens  15237  4sq  16293  symgval  18492  isuhgr  26856  isushgr  26857  isupgr  26880  isumgr  26891  isuspgr  26948  isusgr  26949  isconngr  27977  isconngr1  27978  dispcmp  31212  eulerpart  31748  ballotlemfmpn  31860  bnj66  32240  bnj1234  32393  subfacp1lem6  32540  subfacp1  32541  dfon2lem3  33138  dfon2lem7  33142  frrlem1  33231  nosupdm  33312  f1omptsn  34749  rdgssun  34790  ismblfin  35091  glbconxN  36667  eldioph3  39694  diophrex  39703  cbvcllem  40296  ssfiunibd  41928  aiotajust  43628
  Copyright terms: Public domain W3C validator