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

Theorem rabbidv 2609
Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995.)
Hypothesis
Ref Expression
rabbidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
rabbidv  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  A  |  ch } )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem rabbidv
StepHypRef Expression
1 rabbidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21adantr 271 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
32rabbidva 2608 1  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  A  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    = wceq 1290    e. wcel 1439   {crab 2364
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 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-11 1443  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071
This theorem depends on definitions:  df-bi 116  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-ral 2365  df-rab 2369
This theorem is referenced by:  rabeqbidv  2615  difeq2  3113  seex  4171  mptiniseg  4938  supeq1  6735  supeq2  6738  supeq3  6739  cardcl  6870  isnumi  6871  cardval3ex  6874  carden2bex  6878  genpdflem  7127  genipv  7129  genpelxp  7131  addcomprg  7198  mulcomprg  7200  uzval  9082  ixxval  9375  fzval  9487  hashinfom  10247  hashennn  10249  shftfn  10319  gcdval  11290  lcmval  11384  isprm  11430  istopon  11773  toponsspwpwg  11781  clsval  11872
  Copyright terms: Public domain W3C validator