Theorem abbidv 1624

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

Syntax hints:   -> wi 3   <-> wb 153   = wceq 997  {cab 1509

This theorem is referenced by:  rabbidv 1853  hbsbc1gd 2033  hbsbcgd 2034  csbeq1 2053  cbvcsbv 2054  csbcog 2058  csbconstgf 2061  csbabg 2094  difeq1 2204  difeq2 2205  ifeq1 2416  ifeq2 2417  pweq 2455  sneq 2469  rabsn 2497  unieq 2564  inteq 2590  iineq1 2630  iineq2 2633  dfiun2g 2640  csbopabg 2733  frirr 2981  fr2nr 2982  fr3nr 2983  dmsnop 3385  imasng 3481  fveq1 3780  fveq2 3781  fvres 3791  tz6.12-2 3796  fnrnfv 3816  dfimafn 3818  fnsnfv 3824  fvopabn 3843  fvopab5 3850  abrexexg 3918  rdgeq1 3992  rdgeq2 3993  rdglim2 4007  oarec 4254  qseq1 4346  qseq2 4347  mapvalg 4391  pmvalg 4392  ixpeq1 4414  pw2en 4509  karden 4788  aceq3lem 4794  aceq6a 4803  zorn2lem1 4850  zorn2 4858  cardval 4889  cfval 4971  genpv 5167  iooval2 6392  seq1lem1 6568  limsupval 6618  sumeq1 7072  sumeq2 7075  dfisum 7281  isumval 7282  cncfval 7354  infmap2 7673  tgval 7705  cldval 7751  neifval 7799  neival 7802  lpfval 7827  lpval 7828  opnfval 7942  caufval 8011  lnoval 8497  nmofval 8509  nmoval 8510  nmo0 8535  avril1 8867  pjmval 9321  nmopval 9865  nmfnval 9886  adjval 9897  adjval2 9898  elghomlem1 10467  fiv 10571  homeofval 10610  subsp 10648  qusp 10649  ishoma 10797  ishomb 10798  ismona 10819  isepia 10829  isfuna 10838

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518

Copyright terms: Public domain