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

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

Proof of Theorem rabbidv
StepHypRef Expression
1 rabbidv.1 . . 3 (𝜑 → (𝜓𝜒))
21adantr 272 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32rabbidva 2646 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1314  wcel 1463  {crab 2395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 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 2396  df-rab 2400
This theorem is referenced by:  rabeqbidv  2653  difeq2  3156  seex  4225  mptiniseg  5001  supeq1  6839  supeq2  6842  supeq3  6843  cardcl  7003  isnumi  7004  cardval3ex  7007  carden2bex  7011  genpdflem  7279  genipv  7281  genpelxp  7283  addcomprg  7350  mulcomprg  7352  uzval  9277  ixxval  9619  fzval  9732  hashinfom  10464  hashennn  10466  shftfn  10536  gcdval  11544  lcmval  11640  isprm  11686  istopon  12075  toponsspwpwg  12084  clsval  12175  neival  12207  cnpval  12262  blvalps  12452  blval  12453  limccl  12680  ellimc3apf  12681  eldvap  12703
  Copyright terms: Public domain W3C validator