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

Theorem abbidv 2152
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 (φ → {xψ} = {xχ})
Distinct variable group:   φ,x
Allowed substitution hints:   ψ(x)   χ(x)

Proof of Theorem abbidv
StepHypRef Expression
1 nfv 1418 . 2 xφ
2 abbidv.1 . 2 (φ → (ψχ))
31, 2abbid 2151 1 (φ → {xψ} = {xχ})
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   = wceq 1242  {cab 2023
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 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030
This theorem is referenced by:  cdeqab  2748  csbeq1  2849  sbcel12g  2859  sbceqg  2860  csbeq2d  2868  csbnestgf  2892  csbprc  3256  ifbi  3342  pweq  3354  sneq  3378  csbsng  3422  rabsn  3428  dfopg  3538  opeq1  3540  opeq2  3541  csbunig  3579  unieq  3580  inteq  3609  iineq1  3662  iineq2  3665  dfiin2g  3681  iinrabm  3710  iinxprg  3722  opabbid  3813  csbxpg  4364  csbdmg  4472  imasng  4633  csbrng  4725  iotaeq  4818  iotabi  4819  dfimafn  5165  fnsnfv  5175  fndmin  5217  fliftf  5382  oprabbid  5500  recseq  5862  freceq1  5919  freceq2  5920  frec0g  5922  frecsuclem3  5929  frecsuc  5930  qseq1  6090  qseq2  6091  qsinxp  6118  pitonnlem2  6703  pitonn  6704
  Copyright terms: Public domain W3C validator