ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  abbidv GIF 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 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
abbidv (𝜑 → {𝑥𝜓} = {𝑥𝜒})
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem abbidv
StepHypRef Expression
1 nfv 1421 . 2 𝑥𝜑
2 abbidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2abbid 2154 1 (𝜑 → {𝑥𝜓} = {𝑥𝜒})
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  2754  csbeq1  2855  sbcel12g  2865  sbceqg  2866  csbeq2d  2874  csbnestgf  2898  csbprc  3262  ifbi  3348  pweq  3362  sneq  3386  csbsng  3431  rabsn  3437  dfopg  3547  opeq1  3549  opeq2  3550  csbunig  3588  unieq  3589  inteq  3618  iineq1  3671  iineq2  3674  dfiin2g  3690  iinrabm  3719  iinxprg  3731  opabbid  3822  csbxpg  4421  csbdmg  4529  imasng  4690  csbrng  4782  iotaeq  4875  iotabi  4876  dfimafn  5222  fnsnfv  5232  fndmin  5274  fliftf  5439  oprabbid  5558  recseq  5921  freceq1  5979  freceq2  5980  frec0g  5983  frecsuclem3  5990  frecsuc  5991  qseq1  6154  qseq2  6155  qsinxp  6182  prplnqu  6718  cauappcvgprlemlim  6759  caucvgprprlemell  6783  caucvgprprlemelu  6784  caucvgprprlemcbv  6785  caucvgprprlemval  6786  caucvgprprlemnkeqj  6788  caucvgprprlemml  6792  caucvgprprlemmu  6793  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemopu  6797  caucvgprprlemloc  6801  caucvgprprlemclphr  6803  caucvgprprlemexbt  6804  caucvgprprlem1  6807  caucvgprprlem2  6808  caucvgsr  6886  pitonnlem2  6923  pitonn  6924  recidpipr  6932  nntopi  6968  axcaucvglemval  6971  shftlem  9417  shftfibg  9421  shftdm  9423  shftfib  9424
  Copyright terms: Public domain W3C validator