Theorem rabeqdv 2795

Description: Equality of restricted class abstractions. Deduction form of rabeq 2793. (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

Allowed substitution hints:   ph( x)   ps( x)

Proof of Theorem rabeqdv

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

Syntax hints:   -> wi 4   = wceq 1397   {crab 2513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-rab 2518

This theorem is referenced by:  isacnm  7423  elovmpowrd  11164  dfphi2  12815  lspfval  14426  lsppropd  14470  psrval  14704  cncfval  15325  reldvg  15432  dvfvalap  15434  isuhgrm  15951  isushgrm  15952  uhgreq12g  15956  isuhgropm  15961  uhgr0vb  15964  uhgrun  15966  isupgren  15975  upgrop  15984  isumgren  15985  upgrun  16006  umgrun  16008  isuspgren  16037  isusgren  16038  isuspgropen  16044  isusgropen  16045  isausgren  16047  ausgrusgrben  16048  usgrstrrepeen  16111  vtxdgfi0e  16175  1loopgrvd2fi  16185  1hevtxdg1en  16188  clwwlknonmpo  16308  clwwlknon  16309  clwwlk0on0  16311