Theorem abbidv 2008

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

Syntax hints:   -> wi 3   <-> wb 163   = wceq 1298  {cab 1871

This theorem is referenced by:  rabbidva 2286  hbsbc1gdOLD 2516  hbsbcgdOLD 2518  csbeq1 2542  cbvcsbv 2543  csbcog 2547  csbconstgf 2551  sbcel12g 2552  sbceqdig 2554  csbabgOLD 2589  difeq1OLD 2718  difeq2OLD 2720  ifeq1 2985  ifeq1OLD 2986  ifeq2 2987  ifeq2OLD 2988  pweq 3036  sneq 3054  rabsn 3094  unieq 3185  unieqOLD 3186  inteq 3217  iineq1 3270  iineq2 3274  iineq2OLD 3275  dfiun2gOLD 3284  dfiin2g 3286  iinrab 3318  opabbid 3399  csbopabg 3409  frirr 3634  fr2nr 3635  fr3nr 3859  imasng 4287  dmsnopOLD 4368  fveq1 4680  fveq2 4681  fvres 4691  tz6.12-2 4696  fnrnfv 4718  dfimafn 4720  fnsnfv 4728  fvopabn 4749  fvopab5 4756  fvopab6 4757  abrexexg 4837  iotaeq 5093  iotabi 5094  onopriun 5118  rdgeq1 5142  rdgeq2 5143  rdglim2 5157  oarec 5244  qseq1 5346  qseq2 5347  mapvalg 5389  pmvalg 5390  ixpeq1 5412  pw2en 5505  ordtypelem1 5684  ordtypelem6 5689  ordtype 5691  karden 5856  aceq3lem 5894  aceq6a 5903  zorn2lem1 5950  zorn2 5958  cardval 5975  cfval 6054  genpv 6254  iooval2 7534  limsupval 7772  sumeq1 8242  sumeq2 8245  dfisum 8452  isumval 8453  cncfval 8526  infmap2 8850  tgval 8886  txval 8932  txbas 8933  cldval 8942  neifval 8990  neival 8993  lpfval 9018  lpval 9019  opnfval 9134  caufval 9204  lnoval 9752  nmofval 9764  nmoval 9765  nmo0 9791  ajval 9863  avril1 10142  elghomlem1 10193  fiv 10212  homeofval 10234  subsp 10244  filmapf 10307  isfilmap 10308  pjmval 10871  nmopval 11419  nmfnval 11440  adjval 11451  adjval2 11452  bnj956 12853  bnj1315 13051  altxpeq1 14096  altxpeq2 14097  repfuntw 14502  repcpwti 14503  cbicplem 14508  iscst1 14519  iscst2 14520  iscst4 14522  nZdef 14527  prodeq1 14658  prodeq2 14661  prodeq3 14663  prsubrtr 14763  sallnei 14873  subsp2 14902  qusp 14908  ishoma 15136  ishomb 15137  ismona 15158  isepia 15168  isfuna 15182  tarval2g 15250  vtarsu 15263  dfiin2gOLD 15356  fictblem 15370  fictb 15371  ordtypelem1OLD 15375  ordtypelem6OLD 15380  ordtypeOLD 15382  compfipin0lem 15435  compfipin0 15436  topfneec 15501  neibastop2lem1 15519  neibastop2lem2 15520  neibastop2lem3 15521  neibastop2lem4 15522  fixufil 15576  cnpfillim 15589  tailf 15633  istail 15634  sdclem2 15810  sdc 15811  totbndbnd 15944  ismtyval 15947  heiborlem8 15962  pi1bval 16088  rnghomval 16118  dropab1 16424  dropab2 16425  glbconx 17029  csubspset 17208  lineset 17219  pointset 17222  psubspset 17225  pmapglb2x 17254  polval2 17319  psubclset 17346  pautset 17395

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880

Copyright terms: Public domain