Theorem biabdv 1183

Description: Equivalent wff's yield equal class abstractions (deduction rule).

Hypothesis

Ref	Expression
biabdv.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
biabdv	|- (ph -> {x | ps} = {x | ch})

Distinct variable group(s):   ph,x

Proof of Theorem biabdv

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 |- (ph -> A.xph)
2		biabdv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	biabd 1182	1 |- (ph -> {x | ps} = {x | ch})

Syntax hints:   -> wi 2   <-> wb 127  {cab 1090   = wceq 1091

This theorem is referenced by:  birabdv 1343  difeq1 1582  difeq2 1583  ifeq1 1778  ifeq2 1779  pweq 1800  sneq 1816  unieq 1927  inteq 1968  iineq1 2004  iineq2 2007  frirr 2176  fr2nr 2177  fr3nr 2178  dmsnop 2547  imasn 2616  fveq1 2831  fveq2 2832  fvres 2840  tz6.12-2 2845  fniunfv 2860  fnsnfv 2861  fvopabn 2873  abrexexg 2913  rdgeq1 2972  rdgeq2 2973  rdglim2 2987  qseq1 3225  qseq2 3226  mapvalg 3263  pw2en 3348  karden 3551  aceq3lem 3555  aceq6a 3564  zornlem1 3603  zorn 3611  cardval 3633  cfval 3701  genpv 3896  seqlem1 4662  infmap2 4953  pjmvalt 5245

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099

metamath.org