NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  abbidv GIF version

Theorem abbidv 2467
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 1619 . 2 xφ
2 abbidv.1 . 2 (φ → (ψχ))
31, 2abbid 2466 1 (φ → {x ψ} = {x χ})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176   = wceq 1642  {cab 2339
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346
This theorem is referenced by:  csbeq1  3139  sbcel12g  3151  sbceqg  3152  csbeq2d  3160  csbnestgf  3184  nineq1  3234  pweq  3725  sneq  3744  csbsng  3785  rabsn  3790  csbunig  3899  unieq  3900  inteq  3929  iineq1  3983  iineq2  3986  dfiin2g  4000  iinrab  4028  cnvkeq  4215  ins2keq  4218  ins3keq  4219  imakeq1  4224  imakeq2  4225  p6eq  4238  sikeq  4241  setswith  4321  iotaeq  4347  iotabi  4348  preaddccan2lem1  4454  nnadjoin  4520  tfinnn  4534  opabbid  4624  csbxpg  4813  imaeq1  4937  imaeq2  4938  csbrng  4966  imasn  5018  fnrnfv  5364  dfimafn  5366  fnsnfv  5373  fvco2  5382  oprabbid  5563  clos1eq1  5874  clos1eq2  5875  erth  5968  qseq1  5974  qseq2  5975  mapex  6006  mapvalg  6009  ovmuc  6130  ovce  6172  addccan2nclem2  6264
  Copyright terms: Public domain W3C validator