ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  abbidv Unicode version

Theorem abbidv 2155
Description: Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 10-Aug-1993.)
Hypothesis
Ref Expression
abbidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
abbidv  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)

Proof of Theorem abbidv
StepHypRef Expression
1 nfv 1421 . 2  |-  F/ x ph
2 abbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2abbid 2154 1  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 98    = wceq 1243   {cab 2026
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033
This theorem is referenced by:  cdeqab  2751  csbeq1  2852  sbcel12g  2862  sbceqg  2863  csbeq2d  2871  csbnestgf  2895  csbprc  3259  ifbi  3345  pweq  3359  sneq  3383  csbsng  3428  rabsn  3434  dfopg  3544  opeq1  3546  opeq2  3547  csbunig  3585  unieq  3586  inteq  3615  iineq1  3668  iineq2  3671  dfiin2g  3687  iinrabm  3716  iinxprg  3728  opabbid  3819  csbxpg  4408  csbdmg  4516  imasng  4677  csbrng  4769  iotaeq  4862  iotabi  4863  dfimafn  5209  fnsnfv  5219  fndmin  5261  fliftf  5426  oprabbid  5545  recseq  5908  freceq1  5966  freceq2  5967  frec0g  5970  frecsuclem3  5977  frecsuc  5978  qseq1  6141  qseq2  6142  qsinxp  6169  prplnqu  6699  cauappcvgprlemlim  6740  caucvgprprlemell  6764  caucvgprprlemelu  6765  caucvgprprlemcbv  6766  caucvgprprlemval  6767  caucvgprprlemnkeqj  6769  caucvgprprlemml  6773  caucvgprprlemmu  6774  caucvgprprlemopl  6776  caucvgprprlemlol  6777  caucvgprprlemopu  6778  caucvgprprlemloc  6782  caucvgprprlemclphr  6784  caucvgprprlemexbt  6785  caucvgprprlem1  6788  caucvgprprlem2  6789  caucvgsr  6867  pitonnlem2  6904  pitonn  6905  recidpipr  6913  nntopi  6949  axcaucvglemval  6952  shftlem  9295  shftfibg  9299  shftdm  9301  shftfib  9302
  Copyright terms: Public domain W3C validator