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

Theorem raleq 2558
Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)
Assertion
Ref Expression
raleq  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hint:    ph( x)

Proof of Theorem raleq
StepHypRef Expression
1 nfcv 2225 . 2  |-  F/_ x A
2 nfcv 2225 . 2  |-  F/_ x B
31, 2raleqf 2554 1  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103    = wceq 1287   A.wral 2355
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360
This theorem is referenced by:  raleqi  2562  raleqdv  2564  raleqbi1dv  2566  sbralie  2599  inteq  3673  iineq1  3726  bnd2  3981  frforeq2  4144  weeq2  4156  ordeq  4171  reg2exmid  4323  reg3exmid  4366  omsinds  4406  fncnv  5041  funimaexglem  5058  isoeq4  5537  acexmidlemv  5604  tfrlem1  6020  tfr0dm  6034  tfrlemisucaccv  6037  tfrlemi1  6044  tfrlemi14d  6045  tfrexlem  6046  tfr1onlemsucaccv  6053  tfr1onlemaccex  6060  tfr1onlemres  6061  tfrcllemsucaccv  6066  tfrcllembxssdm  6068  tfrcllemaccex  6073  tfrcllemres  6074  tfrcldm  6075  ac6sfi  6559  fimax2gtri  6562  supeq1  6617  supeq2  6620  isomni  6728  rexanuz  10308  rexfiuz  10309  fimaxre2  10543  setindis  11291  bdsetindis  11293  strcoll2  11307
  Copyright terms: Public domain W3C validator