Theorem cbvabv 2810

Description: Rule used to change bound variables, using implicit substitution. Version of cbvab 2813 with disjoint variable conditions requiring fewer axioms. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2153 and ax-13 2371. (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.

Step	Hyp	Ref	Expression
1		sbco2vv 2099	. . . 4 ⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑)
2		cbvabv.1	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	sbievw 2094	. . . . 5 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
4	3	sbbii 2078	. . . 4 ⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
5	1, 4	bitr3i 276	. . 3 ⊢ ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
6		df-clab 2715	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ [𝑧 / 𝑥]𝜑)
7		df-clab 2715	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜓} ↔ [𝑧 / 𝑦]𝜓)
8	5, 6, 7	3bitr4i 302	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑦 ∣ 𝜓})
9	8	eqriv 2734	1 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540  [wsb 2066   ∈ wcel 2105  {cab 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729

This theorem is referenced by:  cbvrabv  3414  cbvsbcvw  3761  difjust  3899  unjust  3901  injust  3903  uniiunlem  4030  dfif3  4485  pwjust  4546  snjust  4570  intab  4922  intabs  5281  iotajust  6417  cbviotavw  6426  frrlem1  8151  wfrlem1OLD  8188  fsetprcnex  8700  sbth  8937  sbthfi  9046  cardprc  9816  iunfictbso  9950  aceq3lem  9956  isf33lem  10202  axdc3  10290  axdclem  10355  axdc  10357  genpv  10835  ltexpri  10879  recexpr  10887  supsr  10948  hashf1lem2  14249  cvbtrcl  14782  mertens  15677  4sq  16742  symgval  19052  isuhgr  27566  isushgr  27567  isupgr  27590  isumgr  27601  isuspgr  27658  isusgr  27659  isconngr  28689  isconngr1  28690  dispcmp  31949  eulerpart  32489  ballotlemfmpn  32601  bnj66  32979  bnj1234  33132  subfacp1lem6  33286  subfacp1  33287  dfon2lem3  33892  dfon2lem7  33896  nosupcbv  33979  nosupdm  33981  noinfcbv  33994  noinfdm  33996  bj-gabeqis  35199  f1omptsn  35580  rdgssun  35621  ismblfin  35890  glbconxN  37613  sticksstones15  40341  eldioph3  40804  diophrex  40813  cbvcllem  41451  ssfiunibd  43097  aiotajust  44841