Theorem abbidv 1575

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

Syntax hints:   -> wi 3   <-> wb 146   = wceq 955  {cab 1462

This theorem is referenced by:  rabbidv 1803  hbsbc1gd 1980  hbsbcgd 1981  csbeq1 2000  csbcog 2004  csbconstgf 2007  csbabg 2040  difeq1 2150  difeq2 2151  ifeq1 2361  ifeq2 2362  pweq 2400  sneq 2414  rabsn 2442  unieq 2506  inteq 2532  iineq1 2572  iineq2 2575  dfiun2g 2582  csbopabg 2674  frirr 2920  fr2nr 2921  fr3nr 2922  dmsnop 3324  imasng 3420  fveq1 3718  fveq2 3719  fvres 3729  tz6.12-2 3734  fnrnfv 3754  dfimafn 3756  fnsnfv 3762  fvopabn 3781  fvopab5 3788  abrexexg 3856  rdgeq1 3929  rdgeq2 3930  rdglim2 3944  oarec 4189  qseq1 4281  qseq2 4282  mapvalg 4323  pmvalg 4324  ixpeq1 4346  pw2en 4435  karden 4709  aceq3lem 4715  aceq6a 4724  zorn2lem1 4771  zorn2 4779  cardval 4809  cfval 4889  genpv 5085  seq1lem1 6259  iooval2t 6317  limsupvalt 6474  sumeq1 6935  sumeq2 6938  dfisum 7144  isumvalt 7145  cncfval 7216  infmap2 7541  tgvalt 7576  cldval 7626  neifval 7674  neival 7677  lpfval 7702  lpval 7703  opnfval 7819  caufval 7888  lnoval 8375  nmofval 8385  nmoval 8386  nmo0 8411  avril1 8739  pjmvalt 9193  nmopvalt 9739  nmfnvalt 9760  adjvalt 9771  adjval2t 9772  elghomlem1 10338  fiv 10433  homeofval 10462  subsp 10488  qusp 10489  ishoma 10631  ishomb 10632  ismona 10651  isfuna 10664

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471

Copyright terms: Public domain