Theorem cbvrabv 3406

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 2091 and ax-13 2299. (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 2842	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 621	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2904	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3091	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3091	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2806	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1507   ∈ wcel 2048  {cab 2753  {crab 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-rab 3091

This theorem is referenced by:  rabrabi  3408  rru  3675  knatar  6927  oeeulem  8020  ordtypecbv  8768  ordtypelem9  8777  inf3lema  8873  oemapso  8931  oemapvali  8933  tz9.12lem3  9004  cofsmo  9481  enfin2i  9533  fin23lem33  9557  isf32lem11  9575  zorn2g  9715  pwfseqlem1  9870  pwfseqlem3  9872  zsupss  12144  zmin  12151  rpnnen1  12190  hashbc  13614  wrd2f1tovbij  14175  sqrlem7  14459  divalglem5  15598  bitsfzolem  15633  smupp1  15679  gcdcllem3  15700  bezout  15737  eulerth  15966  odzval  15974  pcprecl  16022  pcprendvds  16023  pcpremul  16026  pceulem  16028  prmreclem1  16098  prmreclem5  16102  prmreclem6  16103  4sqlem19  16145  vdwnn  16180  hashbcval  16184  gsumvalx  17728  symgfixelq  18312  efgsdm  18604  efgsfo  18614  ablfaclem3  18949  ltbwe  19956  coe1mul2lem2  20129  smadiadetlem3  20971  pptbas  21310  conncompss  21735  ptcmplem5  22358  ustuqtop  22548  utopsnneip  22550  icccmplem2  23124  minveclem5  23729  ivth  23748  ovolicc2lem5  23815  ovolicc  23817  opnmbllem  23895  vitali  23907  itg2monolem3  24046  elqaa  24604  radcnvle  24701  pserdvlem2  24709  lgamgulmlem5  25302  lgamcvglem  25309  wilth  25340  ftalem6  25347  ttgval  26354  axcontlem11  26453  lfgredgge2  26602  usgredgleordALT  26709  nbusgrf1o  26846  cusgrexg  26919  cusgrfilem2  26931  cusgrfi  26933  vtxdushgrfvedglem  26964  vtxdushgrfvedg  26965  vtxdginducedm1  27018  finsumvtxdg2sstep  27024  wwlksnextbij  27388  wwlksnextbijOLD  27389  rusgrnumwwlks  27470  rusgrnumwwlksOLD  27471  clwlkclwwlkfolem  27507  clwlkclwwlken  27516  clwlkclwwlkenOLD  27517  clwwlknscsh  27576  hashecclwwlkn1  27591  umgrhashecclwwlk  27592  clwlknf1oclwwlknlem2  27597  clwlknf1oclwwlkn  27599  clwlknf1oclwwlknOLD  27601  frgrwopreglem5lem  27844  frgrregorufr0  27848  fusgreghash2wsp  27862  dlwwlknondlwlknonf1o  27906  dlwwlknondlwlknonf1oOLD  27907  ubthlem3  28417  htth  28464  fcobijfs  30200  locfinreflem  30705  ordtconnlem1  30768  dynkin  31028  ddemeas  31097  oddpwdc  31214  eulerpartgbij  31232  eulerpartlemn  31241  eulerpart  31242  ballotlemelo  31348  ballotleme  31357  ballotlem7  31396  reprsuc  31495  hgt750lema  31537  hgt750leme  31538  subfacp1lem6  31977  erdsze  31994  cvmscbv  32050  cvmsiota  32069  cvmlift2lem13  32107  neibastop2  33170  topdifinffin  34006  poimirlem27  34308  mblfinlem1  34318  mblfinlem2  34319  lclkrs2  38069  eldioph4i  38750  rfovcnvf1od  39658  fsovrfovd  39663  fsovcnvlem  39667  nzss  40009  supminfxr2  41122  limcperiod  41286  cncfshiftioo  41551  ioodvbdlimc1lem2  41593  ioodvbdlimc2lem  41595  dvnprodlem1  41607  dvnprod  41610  itgiccshift  41641  itgperiod  41642  stoweidlem49  41711  fourierdlem41  41810  fourierdlem48  41816  fourierdlem49  41817  fourierdlem54  41822  fourierdlem65  41833  fourierdlem70  41838  fourierdlem71  41839  fourierdlem81  41849  fourierdlem89  41857  fourierdlem90  41858  fourierdlem91  41859  fourierdlem92  41860  fourierdlem96  41864  fourierdlem97  41865  fourierdlem98  41866  fourierdlem99  41867  fourierdlem100  41868  fourierdlem103  41871  fourierdlem104  41872  fourierdlem105  41873  fourierdlem108  41876  fourierdlem109  41877  fourierdlem110  41878  fourierdlem112  41880  fourierdlem113  41881  elaa2  41896  etransclem11  41907  etransc  41945  salexct  41994  subsaliuncl  42018  sge0fodjrnlem  42075  meadjiun  42125  ovnsubadd  42231  hoidmv1le  42253  hoidmvlelem3  42256  hoidmvlelem5  42258  ovnhoi  42262  hspmbllem3  42287  hspmbl  42288  opnvonmbl  42293  ovolval4lem2  42309  ovolval5lem2  42312  ovolval5lem3  42313  ovolval5  42314  ovnovol  42318  issmf  42382  incsmf  42396  issmfle  42399  issmfgt  42410  smfadd  42418  decsmf  42420  issmfge  42423  smflimlem4  42427  smflim  42430  smfmul  42447  smflimsuplem2  42472  smflimsuplem5  42475  smflimsuplem7  42477  requad2  43096