Theorem rabbii 1805

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 645	. . 3 |- ((x e. A /\ ps) <-> (x e. A /\ ch))
3	2	abbii 1575	. 2 |- {x | (x e. A /\ ps)} = {x | (x e. A /\ ch)}
4		df-rab 1652	. 2 |- {x e. A | ps} = {x | (x e. A /\ ps)}
5		df-rab 1652	. 2 |- {x e. A | ch} = {x | (x e. A /\ ch)}
6	3, 4, 5	3eqtr4 1505	1 |- {x e. A | ps} = {x e. A | ch}

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 956   e. wcel 958  {cab 1463  {crab 1648

This theorem is referenced by:  rabxfr 2902  reuunixfr 2906  bm2.5ii 3019  nlimon 3122  rankval2 4670  ranksn 4689  hta 4728  kmlem3 4767  infmsup 6068  dfuz 6202  ioopos 6394  isupivth 7290  dsupivthlem 7291  alephsuc3 7585  spwval2 8653  spwval3 8654  spwnex3 8655  pilem3 8673  eff1o 8748  dfbdop2 9786  hhblo 9828  cnlnadjlem5 10004  cdj3lem3 10365  cdj3lem3b 10367

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-rab 1652

Copyright terms: Public domain