Theorem raleq 3317

Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2178, ax-11 2194, and ax-12 2213. (Revised by Steven Nguyen, 30-Apr-2023.) Shorten other proofs. (Revised by Wolf Lammen, 8-Mar-2025.)

Assertion

Ref	Expression
raleq	⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem raleq

Step	Hyp	Ref	Expression
1		rexeq 3316	. . 3 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∃𝑥 ∈ 𝐵 ¬ 𝜑))
2		rexnal 3115	. . 3 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)
3		rexnal 3115	. . 3 ⊢ (∃𝑥 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐵 𝜑)
4	1, 2, 3	3bitr3g 316	. 2 ⊢ (𝐴 = 𝐵 → (¬ ∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐵 𝜑))
5	4	con4bid 320	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1570  ∀wral 3077  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ral 3078  df-rex 3088

This theorem is used by:  raleqi  3318  raleqdv  3320  raleleq  3332  sbralieALT  3340  inteq  4910  iineq1  4969  frsn  5739  fncnv  6613  isoeq4  7328  onminex  7816  tfisg  7865  tfinds  7871  f1oweALT  7984  frxp  8138  frxp2  8161  poseq  8175  frrlem1  8304  frrlem13  8316  tfrlem1  8383  tfrlem12  8397  omeulem1  8590  ixpeq1  8936  undifixp  8962  ac6sfi  9275  frfi  9276  iunfi  9332  indexfi  9349  supeq1  9437  supeq2  9440  brttrcl2  9715  ssttrcl  9716  ttrcltr  9717  setinds  9750  r1filimi  9903  bnd2  9956  bnd2d  9968  acneq  10122  aceq3lem  10199  dfac5lem4  10205  dfac8  10214  dfac9  10215  kmlem1  10229  kmlem10  10238  kmlem13  10241  cfval  10324  axcc2lem  10514  axcc4dom  10519  axdc3lem3  10530  axdc3lem4  10531  ac4c  10554  ac5  10555  ac6sg  10566  zorn2lem7  10580  xrsupsslem  13437  xrinfmsslem  13438  xrsupss  13439  xrinfmss  13440  fsuppmapnn0fiubex  14135  rexanuz  15513  rexfiuz  15515  modfsummod  15961  gcdcllem3  16671  lcmfval  16796  lcmf0val  16797  lcmfunsnlem  16816  coprmprod  16836  coprmproddvds  16838  isprs  18470  drsdirfi  18479  isdrs2  18480  ispos  18488  pospropd  18499  lubeldm  18525  lubval  18528  glbeldm  18538  glbval  18541  istos  18590  isdlat  18696  idressidex  18861  mgmhmpropd  18887  mhmpropd  18987  isghm  19430  cntzval  19535  efgval  19931  iscmn  20003  isomnd  20337  rnghmval  20670  dfrhm2  20704  rhmval0  20705  zrrnghm  20788  isorng  21118  prmidl  21621  lidldvgen  21658  ocvval  21973  isobs  22026  coe1fzgsumd  22622  evl1gsumd  22675  mat0dimcrng  22785  mdetunilem9  22935  ist0  23638  cmpcovf  23709  is1stc  23759  2ndc1stc  23769  isref  23828  txflf  24325  ustuqtop4  24563  iscfilu  24606  ispsmet  24623  ismet  24642  isxmet  24643  cncfval  25209  lebnumlem3  25284  fmcfil  25593  iscfil3  25594  caucfil  25604  iscmet3  25614  cfilres  25617  minveclem3  25750  ovolfiniun  25822  finiunmbl  25865  volfiniun  25868  dvcn  26241  ulmval  26707  ltsval2  28013  ltsres  28019  nolesgn2o  28028  nogesgn1o  28030  nodense  28049  nosupbnd2lem1  28072  noinfbnd2lem1  28087  brslts  28148  madebday  28286  negsprop  28421  mulsprop  28516  onsfi  28742  axtgcont1  28930  nb3grpr  29963  dfconngr1  30789  isconngr  30790  1conngr  30795  frgr0v  30863  isplig  31078  isgrpo  31099  isablo  31148  ocval  31882  acunirnmpt  33253  ismbfm  34884  bnj865  35553  bnj1154  35629  bnj1296  35651  bnj1463  35685  wevgblacfn  35890  derangval  35932  dfon2lem3  36547  dfon2lem7  36551  dfrecs2  36714  dfrdg4  36715  isfne  37127  finixpnum  38528  mblfinlem1  38575  mbfresfi  38584  indexdom  38668  heibor1lem  38743  isexid2  38789  ismndo2  38808  rngomndo  38869  pridl  38971  smprngopr  38986  ispridlc  39004  sn-isghm  43684  setindtrs  44031  dford3lem2  44033  dfac11  44063  rp-intrabeq  44222  rp-unirabeq  44223  rp-brsslt  44423  mnuop123d  45245  relpeq4  45936  trfr  45951  permac8prim  46003  fnchoice  46045  axccdom  46234  axccd  46240  stoweidlem31  47040  stoweidlem57  47066  fourierdlem80  47195  fourierdlem103  47218  fourierdlem104  47219  isvonmbl  47647  paireqne  48592  requad2  48720  smprngprmrng  49435  nelsubc3lem  50177  isthinc  50526  0thincg  50565  cnelsubclem  50710