Theorem cbvrabv 3426

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 2157 and ax-13 2376. (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 2817	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2805	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3416	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3416	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2768	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {cab 2713  {crab 3415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416

This theorem is referenced by:  rru  3762  knatar  7349  oeeulem  8611  cofon1  8682  ordtypecbv  9529  ordtypelem9  9538  inf3lema  9636  oemapso  9694  oemapvali  9696  tz9.12lem3  9801  cofsmo  10281  enfin2i  10333  fin23lem33  10357  isf32lem11  10375  zorn2g  10515  pwfseqlem1  10670  pwfseqlem3  10672  zsupss  12951  zmin  12958  rpnnen1  12997  hashbc  14469  wrd2f1tovbij  14977  01sqrexlem7  15265  divalglem5  16414  bitsfzolem  16451  smupp1  16497  gcdcllem3  16518  bezout  16560  eulerth  16800  odzval  16809  pcprecl  16857  pcprendvds  16858  pcpremul  16861  pceulem  16863  prmreclem1  16934  prmreclem5  16938  prmreclem6  16939  4sqlem19  16981  vdwnn  17016  hashbcval  17020  gsumvalx  18652  symgfixelq  19412  efgsdm  19709  efgsfo  19718  ablfaclem3  20068  ltbwe  22000  coe1mul2lem2  22203  smadiadetlem3  22604  pptbas  22944  conncompss  23369  ptcmplem5  23992  ustuqtop  24183  utopsnneip  24185  icccmplem2  24761  minveclem5  25383  ivth  25405  ovolicc2lem5  25472  ovolicc  25474  opnmbllem  25552  vitali  25564  itg2monolem3  25703  elqaa  26280  radcnvle  26379  pserdvlem2  26388  lgamgulmlem5  26993  lgamcvglem  27000  wilth  27031  ftalem6  27038  precsexlemcbv  28147  ttgval  28800  axcontlem11  28899  lfgredgge2  29049  usgredgleordALT  29159  nbusgrf1o  29296  cusgrexg  29369  cusgrfilem2  29382  cusgrfi  29384  vtxdushgrfvedglem  29415  vtxdushgrfvedg  29416  vtxdginducedm1  29469  finsumvtxdg2sstep  29475  wwlksnextbij  29830  rusgrnumwwlks  29902  clwlkclwwlkfolem  29934  clwlkclwwlken  29939  clwwlknscsh  29989  hashecclwwlkn1  30004  umgrhashecclwwlk  30005  clwlknf1oclwwlknlem2  30009  clwlknf1oclwwlkn  30011  frgrwopreglem5lem  30247  frgrregorufr0  30251  fusgreghash2wsp  30265  dlwwlknondlwlknonf1o  30292  ubthlem3  30799  htth  30845  fcobijfs  32646  elrgspnsubrunlem1  33188  elrgspnsubrun  33190  1arithufd  33509  constrsuc  33718  constrcbvlem  33735  locfinreflem  33817  zarmxt1  33857  zarcmp  33859  ordtconnlem1  33901  dynkin  34144  ddemeas  34213  oddpwdc  34332  eulerpartgbij  34350  eulerpartlemn  34359  eulerpart  34360  ballotlemelo  34466  ballotleme  34475  ballotlem7  34514  reprsuc  34593  hgt750lema  34635  hgt750leme  34636  subfacp1lem6  35153  erdsze  35170  cvmscbv  35226  cvmsiota  35245  cvmlift2lem13  35283  satfv1  35331  neibastop2  36325  weiunfrlem  36428  topdifinffin  37312  poimirlem27  37617  mblfinlem1  37627  mblfinlem2  37628  lclkrs2  41505  aks4d1  42048  sticksstones2  42106  eldioph4i  42782  rfovcnvf1od  43975  fsovrfovd  43980  fsovcnvlem  43984  nzss  44289  supminfxr2  45444  limcperiod  45605  cncfshiftioo  45869  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnprodlem1  45923  dvnprod  45926  itgiccshift  45957  itgperiod  45958  stoweidlem49  46026  fourierdlem41  46125  fourierdlem48  46131  fourierdlem49  46132  fourierdlem54  46137  fourierdlem65  46148  fourierdlem70  46153  fourierdlem71  46154  fourierdlem81  46164  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fourierdlem92  46175  fourierdlem96  46179  fourierdlem97  46180  fourierdlem98  46181  fourierdlem99  46182  fourierdlem100  46183  fourierdlem103  46186  fourierdlem104  46187  fourierdlem105  46188  fourierdlem108  46191  fourierdlem109  46192  fourierdlem110  46193  fourierdlem112  46195  fourierdlem113  46196  elaa2  46211  etransclem11  46222  etransc  46260  salexct  46311  subsaliuncl  46335  sge0fodjrnlem  46393  meadjiun  46443  ovnsubadd  46549  hoidmv1le  46571  hoidmvlelem3  46574  hoidmvlelem5  46576  ovnhoi  46580  hspmbllem3  46605  hspmbl  46606  opnvonmbl  46611  ovolval4lem2  46627  ovolval5lem2  46630  ovolval5lem3  46631  ovolval5  46632  ovnovol  46636  issmf  46705  incsmf  46719  issmfle  46722  issmfgt  46733  smfadd  46742  decsmf  46744  issmfge  46747  smflimlem4  46751  smflim  46754  smfmul  46772  smflimsuplem2  46798  smflimsuplem5  46801  smflimsuplem7  46803  requad2  47585  uspgrlimlem1  47948  grlimgrtri  47956  gpgusgralem  48008  intubeu  48906  unilbeu  48907