Theorem abbidv 1620

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

Syntax hints:   -> wi 3   <-> wb 144   = wceq 992  {cab 1505

This theorem is referenced by:  rabbidv 1852  hbsbc1gd 2031  hbsbcgd 2032  csbeq1 2053  cbvcsbv 2054  csbcog 2058  csbconstgf 2061  csbabg 2095  difeq1 2205  difeq2 2206  ifeq1 2418  ifeq2 2419  pweq 2460  sneq 2475  rabsn 2506  unieq 2576  inteq 2603  iineq1 2644  iineq2 2647  dfiun2g 2654  csbopabg 2752  frirr 2954  fr2nr 2955  fr3nr 3138  imasng 3516  dmsnop 3577  fveq1 3834  fveq2 3835  fvres 3845  tz6.12-2 3850  fnrnfv 3870  dfimafn 3872  fnsnfv 3878  fvopabn 3897  fvopab5 3904  fvopab6 3905  abrexexg 3975  onopriun 4211  rdgeq1 4235  rdgeq2 4236  rdglim2 4250  oarec 4332  qseq1 4428  qseq2 4429  mapvalg 4471  pmvalg 4472  ixpeq1 4494  pw2en 4587  karden 4872  aceq3lem 4878  aceq6a 4887  zorn2lem1 4934  zorn2 4942  cardval 4973  cfval 5056  genpv 5256  iooval2 6493  limsupval 6724  sumeq1 7185  sumeq2 7188  dfisum 7395  isumval 7396  cncfval 7469  infmap2 7793  tgval 7828  cldval 7876  neifval 7924  neival 7927  lpfval 7952  lpval 7953  opnfval 8067  caufval 8137  lnoval 8667  nmofval 8679  nmoval 8680  nmo0 8706  ajval 8778  avril1 9058  pjmval 9514  nmopval 10062  nmfnval 10083  adjval 10094  adjval2 10095  elghomlem1 10667  fiv 10849  sallnei 11016  homeofval 11022  subsp 11056  qusp 11068  ishoma 11242  ishomb 11243  ismona 11264  isepia 11274  isfuna 11288  dfiin2g 11400  fictblem 11422  fictb 11423  ordtypelem1 11427  ordtypelem6 11432  ordtype 11434  compfipin0lem 11492  compfipin0 11493  topfneec 11562  neibastop2lem1 11580  neibastop2lem2 11581  neibastop2lem3 11582  neibastop2lem4 11583  fixufil 11661  cnpfillim 11686  filmapf 11688  isfilmap 11689  tailf 11756  istail 11757  sdclem2 11876  sdc 11877  txval 11972  txbas 11973  totbndbnd 12000  ismtyval 12003  heiborlem8 12018

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514

Copyright terms: Public domain