Theorem rabeqdv 3194

Description: Equality of restricted class abstractions. Deduction form of rabeq 3192. (Contributed by Glauco Siliprandi, 5-Apr-2020.)

Hypothesis

Ref	Expression
rabeqdv.1	|- ( ph -> A = B )

Assertion

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

Distinct variable groups:   x, A   x, B   ph, x

Allowed substitution hint:   ps( x)

Proof of Theorem rabeqdv

Step	Hyp	Ref	Expression
1		rabeqdv.1	. 2 |- ( ph -> A = B )
2		rabeq 3192	. 2 |- ( A = B -> { x e. A | ps } = { x e. B | ps } )
3	1, 2	syl 17	1 |- ( ph -> { x e. A | ps } = { x e. B | ps } )

Syntax hints:   -> wi 4   = wceq 1483   {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-nfc 2753  df-rab 2921

This theorem is referenced by:  rabeqbidv  3195  rabeqbidva  3196  rabsnif  4258  cantnffval  8560  dfphi2  15479  mrisval  16290  coafval  16714  pmtrfval  17870  dprdval  18402  eengv  25859  incistruhgr  25974  isupgr  25979  upgrop  25989  isumgr  25990  upgrun  26013  umgrun  26015  isuspgr  26047  isusgr  26048  isuspgrop  26056  isusgrop  26057  isausgr  26059  ausgrusgrb  26060  usgrstrrepe  26127  lfuhgr1v0e  26146  usgrexmpl  26155  usgrexi  26337  cusgrsize  26350  1loopgrvd2  26399  wwlksn  26729  wspthsn  26735  iswwlksnon  26740  iswspthsnon  26741  clwwlksn  26881  mpstval  31432  pclfvalN  35175  etransclem11  40462