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

Theorem rabbidva2 3424
 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 2862 . 2 (𝜑 → {𝑥 ∣ (𝑥𝐴𝜓)} = {𝑥 ∣ (𝑥𝐵𝜒)})
3 df-rab 3115 . 2 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
4 df-rab 3115 . 2 {𝑥𝐵𝜒} = {𝑥 ∣ (𝑥𝐵𝜒)}
52, 3, 43eqtr4g 2858 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜒})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {cab 2776  {crab 3110 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-rab 3115 This theorem is referenced by:  rabbia2  3425  rabbidva  3426  rabeq  3432  extmptsuppeq  7853  dfac2a  9558  hashbclem  13826  umgrislfupgrlem  26959  wwlksn0s  27691  wwlksnextwrd  27727  wpthswwlks2on  27791  rusgrnumwwlkl1  27798  clwwlknon1  27926  orvcgteel  31901  orvclteel  31906  mapdvalc  39076  mapdval4N  39079  ovncvrrp  43371  ovnsubaddlem1  43377  ovnsubadd  43379  ovncvr2  43418  hspmbl  43436  smflim  43578  smflimsuplem1  43619  smflimsuplem3  43621  smflimsuplem7  43625  smflimsup  43627
 Copyright terms: Public domain W3C validator