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

Theorem riotabidva 7407
Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (rabbidva 3440 analog.) (Contributed by NM, 17-Jan-2012.)
Hypothesis
Ref Expression
riotabidva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
riotabidva (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem riotabidva
StepHypRef Expression
1 riotabidva.1 . . . 4 ((𝜑𝑥𝐴) → (𝜓𝜒))
21pm5.32da 579 . . 3 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32iotabidv 6547 . 2 (𝜑 → (℩𝑥(𝑥𝐴𝜓)) = (℩𝑥(𝑥𝐴𝜒)))
4 df-riota 7388 . 2 (𝑥𝐴 𝜓) = (℩𝑥(𝑥𝐴𝜓))
5 df-riota 7388 . 2 (𝑥𝐴 𝜒) = (℩𝑥(𝑥𝐴𝜒))
63, 4, 53eqtr4g 2800 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  cio 6514  crio 7387
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-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-uni 4913  df-iota 6516  df-riota 7388
This theorem is referenced by:  riotabiia  7408  dfceil2  13876  cidpropd  17755  grpinvpropd  19046  mirval  28678  mirfv  28679  grpoidval  30542  adjval2  31920  riotaeqbidva  32524  xdivval  32886  toslub  32948  tosglb  32950  ringinvval  33225  glbconN  39359  glbconNOLD  39360  cdlemk33N  40892  cdlemk34  40893  cdlemkid4  40917
  Copyright terms: Public domain W3C validator