Theorem raleq 3320

Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2180, ax-11 2197, and ax-12 2216. (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 3319	. . 3 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∃𝑥 ∈ 𝐵 ¬ 𝜑))
2		rexnal 3118	. . 3 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)
3		rexnal 3118	. . 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 3080  ∃wrex 3090

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ral 3081  df-rex 3091

This theorem is used by:  raleqi  3321  raleqdv  3323  raleleq  3335  sbralieALT  3343  inteq  4915  iineq1  4974  frsn  5747  fncnv  6643  isoeq4  7359  onminex  7850  tfisg  7899  tfinds  7905  f1oweALT  8018  frxp  8175  frxp2  8198  poseq  8212  frrlem1  8342  frrlem13  8354  tfrlem1  8421  tfrlem12  8435  omeulem1  8628  ixpeq1  8974  undifixp  9000  ac6sfi  9313  frfi  9314  iunfi  9370  indexfi  9387  supeq1  9474  supeq2  9477  brttrcl2  9752  ssttrcl  9753  ttrcltr  9754  setinds  9787  r1filimi  9940  bnd2  9993  bnd2d  10005  acneq  10161  aceq3lem  10238  dfac5lem4  10244  dfac8  10253  dfac9  10254  kmlem1  10268  kmlem10  10277  kmlem13  10280  cfval  10363  axcc2lem  10553  axcc4dom  10558  axdc3lem3  10569  axdc3lem4  10570  ac4c  10593  ac5  10594  ac6sg  10605  zorn2lem7  10619  xrsupsslem  13477  xrinfmsslem  13478  xrsupss  13479  xrinfmss  13480  fsuppmapnn0fiubex  14175  rexanuz  15557  rexfiuz  15559  modfsummod  16005  gcdcllem3  16715  lcmfval  16840  lcmf0val  16841  lcmfunsnlem  16860  coprmprod  16880  coprmproddvds  16882  isprs  18520  drsdirfi  18529  isdrs2  18530  ispos  18538  pospropd  18549  lubeldm  18575  lubval  18578  glbeldm  18588  glbval  18591  istos  18640  isdlat  18746  idressidex  18911  mgmhmpropd  18937  mhmpropd  19037  isghm  19480  cntzval  19586  efgval  19982  iscmn  20054  isomnd  20388  rnghmval  20721  dfrhm2  20755  rhmval0  20756  zrrnghm  20839  isorng  21169  prmidl  21672  lidldvgen  21709  ocvval  22028  isobs  22081  coe1fzgsumd  22677  evl1gsumd  22730  mat0dimcrng  22840  mdetunilem9  22990  ist0  23693  cmpcovf  23764  is1stc  23814  2ndc1stc  23824  isref  23883  txflf  24380  ustuqtop4  24618  iscfilu  24661  ispsmet  24678  ismet  24697  isxmet  24698  cncfval  25264  lebnumlem3  25339  fmcfil  25648  iscfil3  25649  caucfil  25659  iscmet3  25669  cfilres  25672  minveclem3  25805  ovolfiniun  25877  finiunmbl  25920  volfiniun  25923  dvcn  26296  ulmval  26764  ltsval2  28070  ltsres  28076  nolesgn2o  28085  nogesgn1o  28087  nodense  28106  nosupbnd2lem1  28129  noinfbnd2lem1  28144  brslts  28205  madebday  28343  negsprop  28478  mulsprop  28573  onsfi  28799  axtgcont1  28987  nb3grpr  30020  dfconngr1  30846  isconngr  30847  1conngr  30852  frgr0v  30920  isplig  31135  isgrpo  31156  isablo  31205  ocval  31939  acunirnmpt  33351  ismbfm  34995  bnj865  35664  bnj1154  35740  bnj1296  35762  bnj1463  35796  wevgblacfn  36080  derangval  36140  dfon2lem3  36762  dfon2lem7  36766  dfrecs2  36929  dfrdg4  36930  isfne  37342  finixpnum  38796  mblfinlem1  38843  mbfresfi  38852  indexdom  38936  heibor1lem  39009  isexid2  39055  ismndo2  39074  rngomndo  39135  pridl  39237  smprngopr  39252  ispridlc  39270  sn-isghm  43950  setindtrs  44298  dford3lem2  44300  dfac11  44330  rp-intrabeq  44484  rp-unirabeq  44485  rp-brsslt  44685  mnuop123d  45507  relpeq4  46201  trfr  46216  permac8prim  46268  fnchoice  46320  axccdom  46508  axccd  46514  stoweidlem31  47314  stoweidlem57  47340  fourierdlem80  47469  fourierdlem103  47492  fourierdlem104  47493  isvonmbl  47921  paireqne  48866  requad2  48994  smprngprmrng  49767  nelsubc3lem  50515  isthinc  50885  0thincg  50924  cnelsubcw  51072