ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rabbidva GIF version

Theorem rabbidva 2645
Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 28-Nov-2003.)
Hypothesis
Ref Expression
rabbidva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
rabbidva (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rabbidva
StepHypRef Expression
1 rabbidva.1 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
21ralrimiva 2479 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
3 rabbi 2582 . 2 (∀𝑥𝐴 (𝜓𝜒) ↔ {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
42, 3sylib 121 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1314  wcel 1463  wral 2390  {crab 2394
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-ral 2395  df-rab 2399
This theorem is referenced by:  rabbidv  2646  rabeqbidva  2653  rabbi2dva  3250  rabxfrd  4350  onsucmin  4383  seinxp  4570  fniniseg2  5496  fnniniseg2  5497  f1oresrab  5539  dfinfre  8624  minmax  10893  xrminmax  10926  iooinsup  10938  gcdass  11549  lcmass  11612  bdbl  12492  xmetxpbl  12497
  Copyright terms: Public domain W3C validator