Theorem abbidv 1577

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 971	. 2 |- (ph -> A.xph)
2		abbidv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	abbid 1576	1 |- (ph -> {x | ps} = {x | ch})

Syntax hints:   -> wi 3   <-> wb 146   = wceq 956  {cab 1463

This theorem is referenced by:  rabbidv 1806  hbsbc1gd 1983  hbsbcgd 1984  csbeq1 2003  csbcog 2007  csbconstgf 2010  csbabg 2043  difeq1 2153  difeq2 2154  ifeq1 2364  ifeq2 2365  pweq 2403  sneq 2417  rabsn 2445  unieq 2510  inteq 2536  iineq1 2576  iineq2 2579  dfiun2g 2586  csbopabg 2678  frirr 2924  fr2nr 2925  fr3nr 2926  dmsnop 3328  imasng 3424  fveq1 3723  fveq2 3724  fvres 3734  tz6.12-2 3739  fnrnfv 3759  dfimafn 3761  fnsnfv 3767  fvopabn 3786  fvopab5 3793  abrexexg 3861  rdgeq1 3934  rdgeq2 3935  rdglim2 3949  oarec 4196  qseq1 4288  qseq2 4289  mapvalg 4330  pmvalg 4331  ixpeq1 4353  pw2en 4446  karden 4726  aceq3lem 4732  aceq6a 4741  zorn2lem1 4788  zorn2 4796  cardval 4826  cfval 4906  genpv 5102  seq1lem1 6309  iooval2t 6367  limsupvalt 6529  sumeq1 6982  sumeq2 6985  dfisum 7191  isumvalt 7192  cncfval 7264  infmap2 7581  tgvalt 7616  cldval 7666  neifval 7714  neival 7717  lpfval 7742  lpval 7743  opnfval 7857  caufval 7926  lnoval 8413  nmofval 8425  nmoval 8426  nmo0 8451  avril1 8784  pjmvalt 9238  nmopvalt 9782  nmfnvalt 9803  adjvalt 9814  adjval2t 9815  elghomlem1 10382  fiv 10482  fivOLD 10483  homeofval 10516  subsp 10554  qusp 10555  ishoma 10715  ishomb 10716  ismona 10737  isepia 10747  isfuna 10754

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472

Copyright terms: Public domain