Theorem rabbidva2 3186

Description: Equivalent wff's yield equal restricted class abstractions. (Contributed by Thierry Arnoux, 4-Feb-2017.)

Hypothesis

Ref	Expression
rabbidva2.1	|- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) ) )

Assertion

Ref	Expression
rabbidva2	|- ( ph -> { x e. A | ps } = { x e. B | ch } )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)   B( x)

Proof of Theorem rabbidva2

Step	Hyp	Ref	Expression
1		rabbidva2.1	. . 3 |- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) ) )
2	1	abbidv 2741	. 2 |- ( ph -> { x | ( x e. A /\ ps ) } = { x | ( x e. B /\ ch ) } )
3		df-rab 2921	. 2 |- { x e. A | ps } = { x | ( x e. A /\ ps ) }
4		df-rab 2921	. 2 |- { x e. B | ch } = { x | ( x e. B /\ ch ) }
5	2, 3, 4	3eqtr4g 2681	1 |- ( ph -> { x e. A | ps } = { x e. B | ch } )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   {cab 2608   {crab 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-rab 2921

This theorem is referenced by:  rabbia2  3187  extmptsuppeq  7319  dfac2a  8952  hashbclem  13236  umgrislfupgrlem  26017  wwlksn0s  26746  wwlksnextwrd  26792  wpthswwlks2on  26854  rusgrnumwwlkl1  26863  numclwwlkovf2  27217  orvcgteel  30529  orvclteel  30534  mapdvalc  36918  mapdval4N  36921  ovncvrrp  40778  ovnsubaddlem1  40784  ovnsubadd  40786  ovncvr2  40825  hspmbl  40843  smflim  40985  smflimsuplem1  41026  smflimsuplem3  41028  smflimsuplem7  41032  smflimsup  41034