Theorem abbidv 1569

Description: Equivalent wff's yield equal class abstractions (deduction rule).

Hypothesis

Ref	Expression
abbidv.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
abbidv	|- (ph -> {x | ps} = {x | ch})

Distinct variable group:   ph,x

Proof of Theorem abbidv

Step	Hyp	Ref	Expression
1		ax-17 968	. 2 |- (ph -> A.xph)
2		abbidv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	abbid 1568	1 |- (ph -> {x | ps} = {x | ch})

Syntax hints:   -> wi 3   <-> wb 146   = wceq 953  {cab 1456

This theorem is referenced by:  rabbidv 1797  hbsbc1gd 1973  hbsbcgd 1974  csbeq1 1993  csbcog 1997  csbconstgf 2000  csbabg 2033  difeq1 2143  difeq2 2144  ifeq1 2354  ifeq2 2355  pweq 2393  sneq 2407  rabsn 2435  unieq 2500  inteq 2526  iineq1 2566  iineq2 2569  dfiun2g 2576  csbopabg 2668  frirr 2914  fr2nr 2915  fr3nr 2916  dmsnop 3317  imasng 3408  fveq1 3708  fveq2 3709  fvres 3719  tz6.12-2 3724  fnrnfv 3744  dfimafn 3746  fnsnfv 3752  fvopabn 3771  fvopab5 3778  abrexexg 3846  rdgeq1 3919  rdgeq2 3920  rdglim2 3934  oarec 4180  qseq1 4272  qseq2 4273  mapvalg 4314  pmvalg 4315  ixpeq1 4337  pw2en 4426  karden 4698  aceq3lem 4704  aceq6a 4713  zorn2lem1 4760  zorn2 4768  cardval 4798  cfval 4878  genpv 5074  seq1lem1 6246  iooval2t 6304  limsupvalt 6461  sumeq1 6920  sumeq2 6923  dfisum 7127  isumvalt 7128  cncfval 7199  infmap2 7523  tgvalt 7558  cldval 7608  neifval 7655  neival 7658  lpfval 7683  lpval 7684  opnfval 7797  caufval 7864  lnoval 8347  nmofval 8357  nmoval 8358  nmo0 8383  avril1 8723  pjmvalt 9153  nmopvalt 9699  nmfnvalt 9720  adjvalt 9731  adjval2t 9732  elghomlem1 10287  fiv 10374  homeofval 10403  subsp 10429  qusp 10430  ishoma 10559  ishomb 10560  ismona 10579  isfuna 10592

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465

Copyright terms: Public domain