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

Theorem raleq 2554
Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)
Assertion
Ref Expression
raleq (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem raleq
StepHypRef Expression
1 nfcv 2223 . 2 𝑥𝐴
2 nfcv 2223 . 2 𝑥𝐵
31, 2raleqf 2550 1 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103   = wceq 1285  wral 2353
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358
This theorem is referenced by:  raleqi  2558  raleqdv  2560  raleqbi1dv  2562  sbralie  2595  inteq  3659  iineq1  3712  bnd2  3967  frforeq2  4128  weeq2  4140  ordeq  4155  reg2exmid  4307  reg3exmid  4350  fncnv  5016  funimaexglem  5033  isoeq4  5496  acexmidlemv  5562  tfrlem1  5978  tfr0dm  5992  tfrlemisucaccv  5995  tfrlemi1  6002  tfrlemi14d  6003  tfrexlem  6004  tfr1onlemsucaccv  6011  tfr1onlemaccex  6018  tfr1onlemres  6019  tfrcllemsucaccv  6024  tfrcllembxssdm  6026  tfrcllemaccex  6031  tfrcllemres  6032  tfrcldm  6033  ac6sfi  6455  supeq1  6494  supeq2  6497  rexanuz  10093  rexfiuz  10094  fimaxre2  10328  setindis  11047  bdsetindis  11049  strcoll2  11063
  Copyright terms: Public domain W3C validator