MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvrabv Structured version   Visualization version   GIF version

Theorem cbvrabv 3339
Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. (Contributed by NM, 26-May-1999.)
Hypothesis
Ref Expression
cbvrabv.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvrabv {𝑥𝐴𝜑} = {𝑦𝐴𝜓}
Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvrabv
StepHypRef Expression
1 nfcv 2902 . 2 𝑥𝐴
2 nfcv 2902 . 2 𝑦𝐴
3 nfv 1992 . 2 𝑦𝜑
4 nfv 1992 . 2 𝑥𝜓
5 cbvrabv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
61, 2, 3, 4, 5cbvrab 3338 1 {𝑥𝐴𝜑} = {𝑦𝐴𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1632  {crab 3054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059
This theorem is referenced by:  pwnss  4979  knatar  6770  oeeulem  7850  ordtypecbv  8587  ordtypelem9  8596  inf3lema  8694  oemapso  8752  oemapvali  8754  tz9.12lem3  8825  cofsmo  9283  enfin2i  9335  fin23lem33  9359  isf32lem11  9377  zorn2g  9517  pwfseqlem1  9672  pwfseqlem3  9674  zsupss  11970  zmin  11977  rpnnen1  12013  hashbc  13429  wrd2f1tovbij  13904  sqrlem7  14188  divalglem5  15322  bitsfzolem  15358  smupp1  15404  gcdcllem3  15425  bezout  15462  eulerth  15690  odzval  15698  pcprecl  15746  pcprendvds  15747  pcpremul  15750  pceulem  15752  prmreclem1  15822  prmreclem5  15826  prmreclem6  15827  4sqlem19  15869  vdwnn  15904  hashbcval  15908  gsumvalx  17471  symgfixelq  18053  efgsdm  18343  efgsfo  18352  ablfaclem3  18686  ltbwe  19674  coe1mul2lem2  19840  smadiadetlem3  20676  pptbas  21014  conncompss  21438  ptcmplem5  22061  ustuqtop  22251  utopsnneip  22253  icccmplem2  22827  minveclem5  23404  ivth  23423  ovolicc2lem5  23489  ovolicc  23491  opnmbllem  23569  vitali  23581  itg2monolem3  23718  elqaa  24276  radcnvle  24373  pserdvlem2  24381  lgamgulmlem5  24958  lgamcvglem  24965  wilth  24996  ftalem6  25003  ttgval  25954  axcontlem11  26053  lfgredgge2  26218  usgredgleordALT  26325  nbusgrf1o  26471  cusgrexg  26550  cusgrfilem2  26562  cusgrfi  26564  vtxdushgrfvedglem  26595  vtxdushgrfvedg  26596  vtxdginducedm1  26649  finsumvtxdg2sstep  26655  wlknwwlksnbij2  27001  wlkwwlkbij2  27008  wwlksnextbij  27020  wlksnwwlknvbij  27026  rusgrnumwwlks  27096  clwlkclwwlkfolem  27130  clwlkclwwlken  27135  clwwlknscsh  27193  hashecclwwlkn1  27208  umgrhashecclwwlk  27209  clwlknf1oclwwlknlem2  27226  clwlknf1oclwwlkn  27228  clwlkssizeeqOLD  27230  clwwlkvbijOLD  27263  frgrwopreglem5lem  27474  frgrregorufr0  27478  fusgreghash2wsp  27492  clwwlknonclwlknonen  27523  dlwwlknondlwlknonf1o  27526  ubthlem3  28037  htth  28084  fcobijfs  29810  locfinreflem  30216  ordtconnlem1  30279  dynkin  30539  ddemeas  30608  oddpwdc  30725  eulerpartgbij  30743  eulerpartlemn  30752  eulerpart  30753  ballotlemelo  30858  ballotleme  30867  ballotlem7  30906  reprsuc  31002  hgt750lema  31044  hgt750leme  31045  subfacp1lem6  31474  erdsze  31491  cvmscbv  31547  cvmsiota  31566  cvmlift2lem13  31604  neibastop2  32662  topdifinffin  33507  poimirlem27  33749  mblfinlem1  33759  mblfinlem2  33760  lclkrs2  37331  eldioph4i  37878  rfovcnvf1od  38800  fsovrfovd  38805  fsovcnvlem  38809  nzss  39018  supminfxr2  40197  limcperiod  40363  cncfshiftioo  40608  ioodvbdlimc1lem2  40650  ioodvbdlimc2lem  40652  dvnprodlem1  40664  dvnprod  40667  itgiccshift  40699  itgperiod  40700  stoweidlem49  40769  fourierdlem41  40868  fourierdlem48  40874  fourierdlem49  40875  fourierdlem54  40880  fourierdlem65  40891  fourierdlem70  40896  fourierdlem71  40897  fourierdlem81  40907  fourierdlem89  40915  fourierdlem90  40916  fourierdlem91  40917  fourierdlem92  40918  fourierdlem96  40922  fourierdlem97  40923  fourierdlem98  40924  fourierdlem99  40925  fourierdlem100  40926  fourierdlem103  40929  fourierdlem104  40930  fourierdlem105  40931  fourierdlem108  40934  fourierdlem109  40935  fourierdlem110  40936  fourierdlem112  40938  fourierdlem113  40939  elaa2  40954  etransclem11  40965  etransc  41003  salexct  41055  subsaliuncl  41079  sge0fodjrnlem  41136  meadjiun  41186  ovnsubadd  41292  hoidmv1le  41314  hoidmvlelem3  41317  hoidmvlelem5  41319  ovnhoi  41323  hspmbllem3  41348  hspmbl  41349  opnvonmbl  41354  ovolval4lem2  41370  ovolval5lem2  41373  ovolval5lem3  41374  ovolval5  41375  ovnovol  41379  issmf  41443  incsmf  41457  issmfle  41460  issmfgt  41471  smfadd  41479  decsmf  41481  issmfge  41484  smflimlem4  41488  smflim  41491  smfmul  41508  smflimsuplem2  41533  smflimsuplem5  41536  smflimsuplem7  41538
  Copyright terms: Public domain W3C validator