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

Theorem rabbidva2 3411
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 2807 . 2 (𝜑 → {𝑥 ∣ (𝑥𝐴𝜓)} = {𝑥 ∣ (𝑥𝐵𝜒)})
3 df-rab 3073 . 2 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
4 df-rab 3073 . 2 {𝑥𝐵𝜒} = {𝑥 ∣ (𝑥𝐵𝜒)}
52, 3, 43eqtr4g 2803 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1539  wcel 2106  {cab 2715  {crab 3068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-rab 3073
This theorem is referenced by:  rabbia2  3412  rabbidva  3413  rabeq  3418  extmptsuppeq  8004  dfac2a  9885  hashbclem  14164  umgrislfupgrlem  27492  wwlksn0s  28226  wwlksnextwrd  28262  wpthswwlks2on  28326  rusgrnumwwlkl1  28333  clwwlknon1  28461  orvcgteel  32434  orvclteel  32439  mapdvalc  39643  mapdval4N  39646  ovncvrrp  44102  ovnsubaddlem1  44108  ovnsubadd  44110  ovncvr2  44149  hspmbl  44167  smflim  44312  smflimsuplem1  44353  smflimsuplem3  44355  smflimsuplem7  44359  smflimsup  44361
  Copyright terms: Public domain W3C validator