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

Theorem rabbidva2 3435
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 2806 . 2 (𝜑 → {𝑥 ∣ (𝑥𝐴𝜓)} = {𝑥 ∣ (𝑥𝐵𝜒)})
3 df-rab 3434 . 2 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
4 df-rab 3434 . 2 {𝑥𝐵𝜒} = {𝑥 ∣ (𝑥𝐵𝜒)}
52, 3, 43eqtr4g 2800 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  {cab 2712  {crab 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-rab 3434
This theorem is referenced by:  rabbia2  3436  rabbidva  3440  rabeq  3448  rabeqbidva  3450  extmptsuppeq  8212  dfac2a  10168  hashbclem  14488  umgrislfupgrlem  29154  wwlksn0s  29891  wwlksnextwrd  29927  wpthswwlks2on  29991  rusgrnumwwlkl1  29998  clwwlknon1  30126  orvcgteel  34449  orvclteel  34454  wevgblacfn  35093  mapdvalc  41612  mapdval4N  41615  ovncvrrp  46520  ovnsubaddlem1  46526  ovnsubadd  46528  ovncvr2  46567  hspmbl  46585  smflim  46733  smflimsuplem1  46776  smflimsuplem3  46778  smflimsuplem7  46782  smflimsup  46784
  Copyright terms: Public domain W3C validator