Theorem rabeqdv 3167

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

Hypothesis

Ref	Expression
rabeqdv.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
rabeqdv	⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem rabeqdv

Step	Hyp	Ref	Expression
1		rabeqdv.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		rabeq 3166	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})

Syntax hints:   → wi 4   = wceq 1475  {crab 2900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905

This theorem is referenced by:  rabeqbidv  3168  rabeqbidva  3169  rabsnif  4202  cantnffval  8443  dfphi2  15317  mrisval  16113  coafval  16537  pmtrfval  17693  dprdval  18225  eengv  25659  incistruhgr  25746  isupgr  25751  isumgr  25761  upgrun  25784  umgrun  25786  isausgra  25883  usgraeq12d  25891  usgra0v  25900  usgra1v  25919  clwwlknprop  26300  mpstval  30686  pclfvalN  34193  etransclem11  39138  isuspgr  40382  isusgr  40383  isusgrop  40392  isausgr  40394  ausgrusgrb  40395  lfuhgr1v0e  40480  usgrexmpl  40487  usgrexi  40661  cusgrsize  40670  1loopgrvd2  40718  wwlksn  41040  wspthsn  41046  iswwlksnon  41051  iswspthsnon  41052  clwwlksn  41189