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

Theorem rabbidva2 3434
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 2801 . 2 (𝜑 → {𝑥 ∣ (𝑥𝐴𝜓)} = {𝑥 ∣ (𝑥𝐵𝜒)})
3 df-rab 3433 . 2 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
4 df-rab 3433 . 2 {𝑥𝐵𝜒} = {𝑥 ∣ (𝑥𝐵𝜒)}
52, 3, 43eqtr4g 2797 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  {cab 2709  {crab 3432
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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-rab 3433
This theorem is referenced by:  rabbia2  3435  rabbidva  3439  rabeq  3446  extmptsuppeq  8175  dfac2a  10126  hashbclem  14413  umgrislfupgrlem  28420  wwlksn0s  29153  wwlksnextwrd  29189  wpthswwlks2on  29253  rusgrnumwwlkl1  29260  clwwlknon1  29388  orvcgteel  33535  orvclteel  33540  mapdvalc  40586  mapdval4N  40589  ovncvrrp  45359  ovnsubaddlem1  45365  ovnsubadd  45367  ovncvr2  45406  hspmbl  45424  smflim  45572  smflimsuplem1  45615  smflimsuplem3  45617  smflimsuplem7  45621  smflimsup  45623
  Copyright terms: Public domain W3C validator