Theorem cbvrabv 3411

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 3402	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3402	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2770	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

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

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 3402

This theorem is referenced by:  rru  3739  knatar  7313  oeeulem  8539  cofon1  8610  ordtypecbv  9434  ordtypelem9  9443  inf3lema  9545  oemapso  9603  oemapvali  9605  tz9.12lem3  9713  cofsmo  10191  enfin2i  10243  fin23lem33  10267  isf32lem11  10285  zorn2g  10425  pwfseqlem1  10581  pwfseqlem3  10583  zsupss  12862  zmin  12869  rpnnen1  12908  hashbc  14388  wrd2f1tovbij  14895  01sqrexlem7  15183  divalglem5  16336  bitsfzolem  16373  smupp1  16419  gcdcllem3  16440  bezout  16482  eulerth  16722  odzval  16731  pcprecl  16779  pcprendvds  16780  pcpremul  16783  pceulem  16785  prmreclem1  16856  prmreclem5  16860  prmreclem6  16861  4sqlem19  16903  vdwnn  16938  hashbcval  16942  gsumvalx  18613  symgfixelq  19374  efgsdm  19671  efgsfo  19680  ablfaclem3  20030  ltbwe  22011  coe1mul2lem2  22222  smadiadetlem3  22624  pptbas  22964  conncompss  23389  ptcmplem5  24012  ustuqtop  24202  utopsnneip  24204  icccmplem2  24780  minveclem5  25401  ivth  25423  ovolicc2lem5  25490  ovolicc  25492  opnmbllem  25570  vitali  25582  itg2monolem3  25721  elqaa  26298  radcnvle  26397  pserdvlem2  26406  lgamgulmlem5  27011  lgamcvglem  27018  wilth  27049  ftalem6  27056  precsexlemcbv  28214  bdayons  28284  ttgval  28959  axcontlem11  29059  lfgredgge2  29209  usgredgleordALT  29319  nbusgrf1o  29456  cusgrexg  29529  cusgrfilem2  29542  cusgrfi  29544  vtxdushgrfvedglem  29575  vtxdushgrfvedg  29576  vtxdginducedm1  29629  finsumvtxdg2sstep  29635  wwlksnextbij  29987  rusgrnumwwlks  30062  clwlkclwwlkfolem  30094  clwlkclwwlken  30099  clwwlknscsh  30149  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  clwlknf1oclwwlknlem2  30169  clwlknf1oclwwlkn  30171  frgrwopreglem5lem  30407  frgrregorufr0  30411  fusgreghash2wsp  30425  dlwwlknondlwlknonf1o  30452  ubthlem3  30959  htth  31005  fcobijfs  32810  fcobijfs2  32811  elrgspnsubrunlem1  33340  elrgspnsubrun  33342  1arithufd  33640  extvfvcl  33712  mplvrpmfgalem  33720  constrsuc  33915  constrcbvlem  33932  locfinreflem  34017  zarmxt1  34057  zarcmp  34059  ordtconnlem1  34101  dynkin  34344  ddemeas  34413  oddpwdc  34531  eulerpartgbij  34549  eulerpartlemn  34558  eulerpart  34559  ballotlemelo  34665  ballotleme  34674  ballotlem7  34713  reprsuc  34792  hgt750lema  34834  hgt750leme  34835  fineqvnttrclse  35299  onvf1odlem3  35318  subfacp1lem6  35398  erdsze  35415  cvmscbv  35471  cvmsiota  35490  cvmlift2lem13  35528  satfv1  35576  neibastop2  36574  weiunfrlem  36677  topdifinffin  37600  poimirlem27  37895  mblfinlem1  37905  mblfinlem2  37906  lclkrs2  41913  aks4d1  42456  sticksstones2  42514  eldioph4i  43166  rfovcnvf1od  44357  fsovrfovd  44362  fsovcnvlem  44366  nzss  44670  supminfxr2  45824  limcperiod  45985  cncfshiftioo  46247  ioodvbdlimc1lem2  46287  ioodvbdlimc2lem  46289  dvnprodlem1  46301  dvnprod  46304  itgiccshift  46335  itgperiod  46336  stoweidlem49  46404  fourierdlem41  46503  fourierdlem48  46509  fourierdlem49  46510  fourierdlem54  46515  fourierdlem65  46526  fourierdlem70  46531  fourierdlem71  46532  fourierdlem81  46542  fourierdlem89  46550  fourierdlem90  46551  fourierdlem91  46552  fourierdlem92  46553  fourierdlem96  46557  fourierdlem97  46558  fourierdlem98  46559  fourierdlem99  46560  fourierdlem100  46561  fourierdlem103  46564  fourierdlem104  46565  fourierdlem105  46566  fourierdlem108  46569  fourierdlem109  46570  fourierdlem110  46571  fourierdlem112  46573  fourierdlem113  46574  elaa2  46589  etransclem11  46600  etransc  46638  salexct  46689  subsaliuncl  46713  sge0fodjrnlem  46771  meadjiun  46821  ovnsubadd  46927  hoidmv1le  46949  hoidmvlelem3  46952  hoidmvlelem5  46954  ovnhoi  46958  hspmbllem3  46983  hspmbl  46984  opnvonmbl  46989  ovolval4lem2  47005  ovolval5lem2  47008  ovolval5lem3  47009  ovolval5  47010  ovnovol  47014  issmf  47083  incsmf  47097  issmfle  47100  issmfgt  47111  smfadd  47120  decsmf  47122  issmfge  47125  smflimlem4  47129  smflim  47132  smfmul  47150  smflimsuplem2  47176  smflimsuplem5  47179  smflimsuplem7  47181  requad2  47980  uspgrlimlem1  48345  grlimedgclnbgr  48352  grlimgrtri  48360  gpgusgralem  48413  intubeu  49340  unilbeu  49341