Theorem rabbii 1808

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

Hypothesis

Ref	Expression
rabbii.1	|- (x e. A -> (ps <-> ch))

Assertion

Ref	Expression
rabbii	|- {x e. A | ps} = {x e. A | ch}

Proof of Theorem rabbii

Step	Hyp	Ref	Expression
1		rabbii.1	. . . 4 |- (x e. A -> (ps <-> ch))
2	1	pm5.32i 647	. . 3 |- ((x e. A /\ ps) <-> (x e. A /\ ch))
3	2	abbii 1578	. 2 |- {x | (x e. A /\ ps)} = {x | (x e. A /\ ch)}
4		df-rab 1655	. 2 |- {x e. A | ps} = {x | (x e. A /\ ps)}
5		df-rab 1655	. 2 |- {x e. A | ch} = {x | (x e. A /\ ch)}
6	3, 4, 5	3eqtr4 1508	1 |- {x e. A | ps} = {x e. A | ch}

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 958   e. wcel 960  {cab 1466  {crab 1651

This theorem is referenced by:  rabxfr 2908  reuunixfr 2912  bm2.5ii 3025  nlimon 3128  rankval2 4680  ranksn 4699  hta 4738  kmlem3 4777  infmsup 6070  dfuz 6204  ioopos 6395  isupivth 7290  dsupivthlem 7291  alephsuc3 7587  spwval2 8649  spwval3 8650  spwnex3 8651  pilem3 8668  eff1o 8743  dfbdop2 9781  hhblo 9823  cnlnadjlem5 9999  cdj3lem3 10360  cdj3lem3b 10362

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-rab 1655

Copyright terms: Public domain