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

Theorem abbidv 2202
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 1464 . 2  |-  F/ x ph
2 abbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2abbid 2201 1  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103    = wceq 1287   {cab 2071
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-11 1440  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078
This theorem is referenced by:  rabbidva2  2602  cdeqab  2819  csbeq1  2925  sbcel12g  2935  sbceqg  2936  csbeq2d  2944  csbnestgf  2969  csbprc  3316  ifbi  3397  pweq  3418  sneq  3442  csbsng  3486  rabsn  3492  dfopg  3603  opeq1  3605  opeq2  3606  csbunig  3644  unieq  3645  inteq  3674  iineq1  3727  iineq2  3730  dfiin2g  3746  iinrabm  3775  iinxprg  3787  opabbid  3878  dcextest  4369  csbxpg  4487  csbdmg  4598  imasng  4764  csbrng  4858  iotaeq  4954  iotabi  4955  dfimafn  5316  fnsnfv  5326  fndmin  5369  fliftf  5539  oprabbid  5659  recseq  6025  freceq1  6111  freceq2  6112  frec0g  6116  freccllem  6121  frecfcllem  6123  frecsuclem  6125  frecsuc  6126  qseq1  6292  qseq2  6293  qsinxp  6320  mapvalg  6367  snexxph  6608  prplnqu  7123  cauappcvgprlemlim  7164  caucvgprprlemell  7188  caucvgprprlemelu  7189  caucvgprprlemcbv  7190  caucvgprprlemval  7191  caucvgprprlemnkeqj  7193  caucvgprprlemml  7197  caucvgprprlemmu  7198  caucvgprprlemopl  7200  caucvgprprlemlol  7201  caucvgprprlemopu  7202  caucvgprprlemloc  7206  caucvgprprlemclphr  7208  caucvgprprlemexbt  7209  caucvgprprlem1  7212  caucvgprprlem2  7213  caucvgsr  7291  pitonnlem2  7328  pitonn  7329  recidpipr  7337  nntopi  7373  axcaucvglemval  7376  shftlem  10147  shftfibg  10151  shftdm  10153  shftfib  10154  negfi  10554
  Copyright terms: Public domain W3C validator