Theorem abbidv 2468

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

Step	Hyp	Ref	Expression
1		nfv 1619	. 2 |- F/xph
2		abbidv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	abbid 2467	1 |- (ph -> {x | ps} = {x | ch})

Syntax hints:   -> wi 4   <-> wb 176   = wceq 1642  {cab 2339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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  3140  sbcel12g  3152  sbceqg  3153  csbeq2d  3161  csbnestgf  3185  nineq1  3235  pweq  3726  sneq  3745  csbsng  3786  rabsn  3791  csbunig  3900  unieq  3901  inteq  3930  iineq1  3984  iineq2  3987  dfiin2g  4001  iinrab  4029  cnvkeq  4216  ins2keq  4219  ins3keq  4220  imakeq1  4225  imakeq2  4226  p6eq  4239  sikeq  4242  setswith  4322  iotaeq  4348  iotabi  4349  preaddccan2lem1  4455  nnadjoin  4521  tfinnn  4535  opabbid  4625  csbxpg  4814  imaeq1  4938  imaeq2  4939  csbrng  4967  imasn  5019  fnrnfv  5365  dfimafn  5367  fnsnfv  5374  fvco2  5383  oprabbid  5564  clos1eq1  5875  clos1eq2  5876  erth  5969  qseq1  5975  qseq2  5976  mapex  6007  mapvalg  6010  ovmuc  6131  ovce  6173  addccan2nclem2  6265