Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rabbidva2 Structured version   Visualization version   GIF version

Theorem rabbidva2 3162
 Description: Equivalent wff's yield equal restricted class abstractions. (Contributed by Thierry Arnoux, 4-Feb-2017.)
Hypothesis
Ref Expression
rabbidva2.1 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐵𝜒)))
Assertion
Ref Expression
rabbidva2 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜒})
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem rabbidva2
StepHypRef Expression
1 rabbidva2.1 . . 3 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐵𝜒)))
21abbidv 2728 . 2 (𝜑 → {𝑥 ∣ (𝑥𝐴𝜓)} = {𝑥 ∣ (𝑥𝐵𝜒)})
3 df-rab 2905 . 2 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
4 df-rab 2905 . 2 {𝑥𝐵𝜒} = {𝑥 ∣ (𝑥𝐵𝜒)}
52, 3, 43eqtr4g 2669 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜒})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {cab 2596  {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-rab 2905 This theorem is referenced by:  extmptsuppeq  7206  dfac2a  8835  hashbclem  13093  umgrislfupgrlem  25788  isusgra0  25876  wwlkn0s  26233  wwlkextwrd  26256  rusgranumwlkl1  26474  rusgranumwlklem3  26478  numclwwlkovf2  26611  orvcgteel  29856  orvclteel  29861  mapdvalc  35936  mapdval4N  35939  rabbia2  38309  ovncvrrp  39454  ovnsubaddlem1  39460  ovnsubadd  39462  ovncvr2  39501  hspmbl  39519  smflim  39663  wwlksn0s  41057  wwlksnextwrd  41103  wpthswwlks2on  41164  rusgrnumwwlkl1  41172  av-numclwwlkovf2  41515
 Copyright terms: Public domain W3C validator