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

Theorem riotabidva 7334
Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (rabbidva 3415 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 580 . . 3 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32iotabidv 6481 . 2 (𝜑 → (℩𝑥(𝑥𝐴𝜓)) = (℩𝑥(𝑥𝐴𝜒)))
4 df-riota 7314 . 2 (𝑥𝐴 𝜓) = (℩𝑥(𝑥𝐴𝜓))
5 df-riota 7314 . 2 (𝑥𝐴 𝜒) = (℩𝑥(𝑥𝐴𝜒))
63, 4, 53eqtr4g 2802 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  cio 6447  crio 7313
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-in 3918  df-ss 3928  df-uni 4867  df-iota 6449  df-riota 7314
This theorem is referenced by:  riotabiia  7335  dfceil2  13745  cidpropd  17591  grpinvpropd  18823  mirval  27600  mirfv  27601  grpoidval  29458  adjval2  30836  riotaeqbidva  31427  xdivval  31778  toslub  31836  tosglb  31838  ringinvval  32075  glbconN  37842  glbconNOLD  37843  cdlemk33N  39375  cdlemk34  39376  cdlemkid4  39400
  Copyright terms: Public domain W3C validator