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

Theorem abbidv 2197
Description: Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 10-Aug-1993.)
Hypothesis
Ref Expression
abbidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
abbidv (𝜑 → {𝑥𝜓} = {𝑥𝜒})
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem abbidv
StepHypRef Expression
1 nfv 1462 . 2 𝑥𝜑
2 abbidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2abbid 2196 1 (𝜑 → {𝑥𝜓} = {𝑥𝜒})
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103   = wceq 1285  {cab 2068
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075
This theorem is referenced by:  cdeqab  2806  csbeq1  2912  sbcel12g  2922  sbceqg  2923  csbeq2d  2931  csbnestgf  2955  csbprc  3296  ifbi  3377  pweq  3393  sneq  3417  csbsng  3461  rabsn  3467  dfopg  3576  opeq1  3578  opeq2  3579  csbunig  3617  unieq  3618  inteq  3647  iineq1  3700  iineq2  3703  dfiin2g  3719  iinrabm  3748  iinxprg  3760  opabbid  3851  csbxpg  4447  csbdmg  4557  imasng  4720  csbrng  4812  iotaeq  4905  iotabi  4906  dfimafn  5254  fnsnfv  5264  fndmin  5306  fliftf  5470  oprabbid  5589  recseq  5955  freceq1  6041  freceq2  6042  frec0g  6046  freccllem  6051  frecfcllem  6053  frecsuclem  6055  frecsuc  6056  qseq1  6220  qseq2  6221  qsinxp  6248  prplnqu  6872  cauappcvgprlemlim  6913  caucvgprprlemell  6937  caucvgprprlemelu  6938  caucvgprprlemcbv  6939  caucvgprprlemval  6940  caucvgprprlemnkeqj  6942  caucvgprprlemml  6946  caucvgprprlemmu  6947  caucvgprprlemopl  6949  caucvgprprlemlol  6950  caucvgprprlemopu  6951  caucvgprprlemloc  6955  caucvgprprlemclphr  6957  caucvgprprlemexbt  6958  caucvgprprlem1  6961  caucvgprprlem2  6962  caucvgsr  7040  pitonnlem2  7077  pitonn  7078  recidpipr  7086  nntopi  7122  axcaucvglemval  7125  shftlem  9842  shftfibg  9846  shftdm  9848  shftfib  9849  negfi  10248
  Copyright terms: Public domain W3C validator