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

Theorem abbidv 2235
Description: Equivalent wff's yield equal class abstractions (deduction form). (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 1493 . 2  |-  F/ x ph
2 abbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2abbid 2234 1  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    = wceq 1316   {cab 2103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110
This theorem is referenced by:  rabbidva2  2647  cdeqab  2872  csbeq1  2978  sbcel12g  2988  sbceqg  2989  csbeq2d  2997  csbnestgf  3022  csbprc  3378  ifbi  3462  pweq  3483  sneq  3508  csbsng  3554  rabsn  3560  dfopg  3673  opeq1  3675  opeq2  3676  csbunig  3714  unieq  3715  inteq  3744  iineq1  3797  iineq2  3800  dfiin2g  3816  iinrabm  3845  iinxprg  3857  opabbid  3963  dcextest  4465  csbxpg  4590  csbdmg  4703  imasng  4874  csbrng  4970  iotaeq  5066  iotabi  5067  dfimafn  5438  fnsnfv  5448  fndmin  5495  fliftf  5668  oprabbid  5792  recseq  6171  freceq1  6257  freceq2  6258  frec0g  6262  freccllem  6267  frecfcllem  6269  frecsuclem  6271  frecsuc  6272  qseq1  6445  qseq2  6446  qsinxp  6473  mapvalg  6520  ixpsnval  6563  ixpeq1  6571  snexxph  6806  fival  6826  prplnqu  7396  cauappcvgprlemlim  7437  caucvgprprlemell  7461  caucvgprprlemelu  7462  caucvgprprlemcbv  7463  caucvgprprlemval  7464  caucvgprprlemnkeqj  7466  caucvgprprlemml  7470  caucvgprprlemmu  7471  caucvgprprlemopl  7473  caucvgprprlemlol  7474  caucvgprprlemopu  7475  caucvgprprlemloc  7479  caucvgprprlemclphr  7481  caucvgprprlemexbt  7482  caucvgprprlem1  7485  caucvgprprlem2  7486  caucvgsr  7578  pitonnlem2  7623  pitonn  7624  recidpipr  7632  nntopi  7670  axcaucvglemval  7673  shftlem  10543  shftfibg  10547  shftdm  10549  shftfib  10550  negfi  10954  tgval  12129
  Copyright terms: Public domain W3C validator