Theorem cbvrabv 3400

Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2163 and ax-13 2377. (Revised by Steven Nguyen, 4-Dec-2022.)

Hypothesis

Ref	Expression
cbvrabv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvrabv	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvrabv

Step	Hyp	Ref	Expression
1		eleq1w 2820	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 633	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2807	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3391	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3391	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2770	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {cab 2715  {crab 3390

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-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391

This theorem is referenced by:  rru  3726  knatar  7305  oeeulem  8530  cofon1  8601  ordtypecbv  9425  ordtypelem9  9434  inf3lema  9536  oemapso  9594  oemapvali  9596  tz9.12lem3  9704  cofsmo  10182  enfin2i  10234  fin23lem33  10258  isf32lem11  10276  zorn2g  10416  pwfseqlem1  10572  pwfseqlem3  10574  zsupss  12878  zmin  12885  rpnnen1  12924  hashbc  14406  wrd2f1tovbij  14913  01sqrexlem7  15201  divalglem5  16357  bitsfzolem  16394  smupp1  16440  gcdcllem3  16461  bezout  16503  eulerth  16744  odzval  16753  pcprecl  16801  pcprendvds  16802  pcpremul  16805  pceulem  16807  prmreclem1  16878  prmreclem5  16882  prmreclem6  16883  4sqlem19  16925  vdwnn  16960  hashbcval  16964  gsumvalx  18635  symgfixelq  19399  efgsdm  19696  efgsfo  19705  ablfaclem3  20055  ltbwe  22032  coe1mul2lem2  22243  smadiadetlem3  22643  pptbas  22983  conncompss  23408  ptcmplem5  24031  ustuqtop  24221  utopsnneip  24223  icccmplem2  24799  minveclem5  25410  ivth  25431  ovolicc2lem5  25498  ovolicc  25500  opnmbllem  25578  vitali  25590  itg2monolem3  25729  elqaa  26299  radcnvle  26398  pserdvlem2  26406  lgamgulmlem5  27010  lgamcvglem  27017  wilth  27048  ftalem6  27055  precsexlemcbv  28212  bdayons  28282  ttgval  28957  axcontlem11  29057  lfgredgge2  29207  usgredgleordALT  29317  nbusgrf1o  29454  cusgrexg  29527  cusgrfilem2  29540  cusgrfi  29542  vtxdushgrfvedglem  29573  vtxdushgrfvedg  29574  vtxdginducedm1  29627  finsumvtxdg2sstep  29633  wwlksnextbij  29985  rusgrnumwwlks  30060  clwlkclwwlkfolem  30092  clwlkclwwlken  30097  clwwlknscsh  30147  hashecclwwlkn1  30162  umgrhashecclwwlk  30163  clwlknf1oclwwlknlem2  30167  clwlknf1oclwwlkn  30169  frgrwopreglem5lem  30405  frgrregorufr0  30409  fusgreghash2wsp  30423  dlwwlknondlwlknonf1o  30450  ubthlem3  30958  htth  31004  fcobijfs  32809  fcobijfs2  32810  elrgspnsubrunlem1  33323  elrgspnsubrun  33325  1arithufd  33623  extvfvcl  33695  mplvrpmfgalem  33703  constrsuc  33898  constrcbvlem  33915  locfinreflem  34000  zarmxt1  34040  zarcmp  34042  ordtconnlem1  34084  dynkin  34327  ddemeas  34396  oddpwdc  34514  eulerpartgbij  34532  eulerpartlemn  34541  eulerpart  34542  ballotlemelo  34648  ballotleme  34657  ballotlem7  34696  reprsuc  34775  hgt750lema  34817  hgt750leme  34818  fineqvnttrclse  35284  onvf1odlem3  35303  subfacp1lem6  35383  erdsze  35400  cvmscbv  35456  cvmsiota  35475  cvmlift2lem13  35513  satfv1  35561  neibastop2  36559  weiunfrlem  36662  topdifinffin  37678  poimirlem27  37982  mblfinlem1  37992  mblfinlem2  37993  lclkrs2  42000  aks4d1  42542  sticksstones2  42600  eldioph4i  43258  rfovcnvf1od  44449  fsovrfovd  44454  fsovcnvlem  44458  nzss  44762  supminfxr2  45915  limcperiod  46076  cncfshiftioo  46338  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvnprodlem1  46392  dvnprod  46395  itgiccshift  46426  itgperiod  46427  stoweidlem49  46495  fourierdlem41  46594  fourierdlem48  46600  fourierdlem49  46601  fourierdlem54  46606  fourierdlem65  46617  fourierdlem70  46622  fourierdlem71  46623  fourierdlem81  46633  fourierdlem89  46641  fourierdlem90  46642  fourierdlem91  46643  fourierdlem92  46644  fourierdlem96  46648  fourierdlem97  46649  fourierdlem98  46650  fourierdlem99  46651  fourierdlem100  46652  fourierdlem103  46655  fourierdlem104  46656  fourierdlem105  46657  fourierdlem108  46660  fourierdlem109  46661  fourierdlem110  46662  fourierdlem112  46664  fourierdlem113  46665  elaa2  46680  etransclem11  46691  etransc  46729  salexct  46780  subsaliuncl  46804  sge0fodjrnlem  46862  meadjiun  46912  ovnsubadd  47018  hoidmv1le  47040  hoidmvlelem3  47043  hoidmvlelem5  47045  ovnhoi  47049  hspmbllem3  47074  hspmbl  47075  opnvonmbl  47080  ovolval4lem2  47096  ovolval5lem2  47099  ovolval5lem3  47100  ovolval5  47101  ovnovol  47105  issmf  47174  incsmf  47188  issmfle  47191  issmfgt  47202  smfadd  47211  decsmf  47213  issmfge  47216  smflimlem4  47220  smflim  47223  smfmul  47241  smflimsuplem2  47267  smflimsuplem5  47270  smflimsuplem7  47272  requad2  48111  uspgrlimlem1  48476  grlimedgclnbgr  48483  grlimgrtri  48491  gpgusgralem  48544  intubeu  49471  unilbeu  49472