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

Theorem riotabidva 6882
Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (rabbidva 3401 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 576 . . 3 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32iotabidv 6107 . 2 (𝜑 → (℩𝑥(𝑥𝐴𝜓)) = (℩𝑥(𝑥𝐴𝜒)))
4 df-riota 6866 . 2 (𝑥𝐴 𝜓) = (℩𝑥(𝑥𝐴𝜓))
5 df-riota 6866 . 2 (𝑥𝐴 𝜒) = (℩𝑥(𝑥𝐴𝜒))
63, 4, 53eqtr4g 2886 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1658  wcel 2166  cio 6084  crio 6865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rex 3123  df-uni 4659  df-iota 6086  df-riota 6866
This theorem is referenced by:  riotabiia  6883  dfceil2  12935  cidpropd  16722  grpinvpropd  17844  mirval  25967  mirfv  25968  grpoidval  27923  adjval2  29305  xdivval  30172  toslub  30213  tosglb  30215  ringinvval  30337  glbconN  35452  cdlemk33N  36984  cdlemk34  36985  cdlemkid4  37009
  Copyright terms: Public domain W3C validator