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

Theorem raleq 2672
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 2319 . 2 𝑥𝐴
2 nfcv 2319 . 2 𝑥𝐵
31, 2raleqf 2668 1 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105   = wceq 1353  wral 2455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460
This theorem is referenced by:  raleqi  2676  raleqdv  2678  raleqbi1dv  2680  sbralie  2721  inteq  3845  iineq1  3898  bnd2  4170  frforeq2  4342  weeq2  4354  ordeq  4369  reg2exmid  4532  reg3exmid  4576  omsinds  4618  fncnv  5278  funimaexglem  5295  isoeq4  5799  acexmidlemv  5867  tfrlem1  6303  tfr0dm  6317  tfrlemisucaccv  6320  tfrlemi1  6327  tfrlemi14d  6328  tfrexlem  6329  tfr1onlemsucaccv  6336  tfr1onlemaccex  6343  tfr1onlemres  6344  tfrcllemsucaccv  6349  tfrcllembxssdm  6351  tfrcllemaccex  6356  tfrcllemres  6357  tfrcldm  6358  ixpeq1  6703  ac6sfi  6892  fimax2gtri  6895  dcfi  6974  supeq1  6979  supeq2  6982  nnnninfeq2  7121  isomni  7128  ismkv  7145  iswomni  7157  sup3exmid  8900  rexanuz  10978  rexfiuz  10979  fimaxre2  11216  modfsummod  11447  mhmpropd  12744  iscmn  12920  srgideu  12978  cnprcl2k  13366  ispsmet  13483  ismet  13504  isxmet  13505  cncfval  13719  dvcn  13824  setindis  14368  bdsetindis  14370  strcoll2  14384  strcollnfALT  14387
  Copyright terms: Public domain W3C validator