Theorem raleq 3320

Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2176, ax-11 2192, 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 3319	. . 3 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∃𝑥 ∈ 𝐵 ¬ 𝜑))
2		rexnal 3117	. . 3 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)
3		rexnal 3117	. . 3 ⊢ (∃𝑥 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐵 𝜑)
4	1, 2, 3	3bitr3g 316	. 2 ⊢ (𝐴 = 𝐵 → (¬ ∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐵 𝜑))
5	4	con4bid 320	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1570  ∀wral 3079  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ral 3080  df-rex 3090

This theorem is referenced by:  raleqi  3321  raleqdv  3323  raleleq  3335  sbralieALT  3343  inteq  4915  iineq1  4974  frsn  5749  fncnv  6609  isoeq4  7318  onminex  7797  tfisg  7846  tfinds  7852  f1oweALT  7965  frxp  8118  frxp2  8136  poseq  8150  frrlem1  8279  frrlem13  8291  tfrlem1  8358  tfrlem12  8372  omeulem1  8563  ixpeq1  8902  undifixp  8928  ac6sfi  9240  frfi  9241  iunfi  9296  indexfi  9313  supeq1  9401  supeq2  9404  brttrcl2  9679  ssttrcl  9680  ttrcltr  9681  setinds  9714  bnd2  9875  acneq  10023  aceq3lem  10100  dfac5lem4  10106  dfac8  10115  dfac9  10116  kmlem1  10130  kmlem10  10139  kmlem13  10142  cfval  10225  axcc2lem  10415  axcc4dom  10420  axdc3lem3  10431  axdc3lem4  10432  ac4c  10455  ac5  10456  ac6sg  10467  zorn2lem7  10481  xrsupsslem  13328  xrinfmsslem  13329  xrsupss  13330  xrinfmss  13331  fsuppmapnn0fiubex  14024  rexanuz  15393  rexfiuz  15395  modfsummod  15842  gcdcllem3  16554  lcmfval  16674  lcmf0val  16675  lcmfunsnlem  16694  coprmprod  16714  coprmproddvds  16716  isprs  18347  drsdirfi  18356  isdrs2  18357  ispos  18365  pospropd  18376  lubeldm  18402  lubval  18405  glbeldm  18415  glbval  18418  istos  18467  isdlat  18573  mgmhmpropd  18751  mhmpropd  18845  isghm  19281  cntzval  19386  efgval  19782  iscmn  19854  isomnd  20188  rnghmval  20518  dfrhm2  20552  rhmval0  20553  zrrnghm  20635  isorng  20964  prmidl  21465  lidldvgen  21502  ocvval  21817  isobs  21870  coe1fzgsumd  22464  evl1gsumd  22517  mat0dimcrng  22627  mdetunilem9  22777  ist0  23477  cmpcovf  23548  is1stc  23598  2ndc1stc  23608  isref  23666  txflf  24163  ustuqtop4  24401  iscfilu  24444  ispsmet  24461  ismet  24480  isxmet  24481  cncfval  25047  lebnumlem3  25122  fmcfil  25431  iscfil3  25432  caucfil  25442  iscmet3  25452  cfilres  25455  minveclem3  25588  ovolfiniun  25660  finiunmbl  25703  volfiniun  25706  dvcn  26080  ulmval  26543  ltsval2  27820  ltsres  27826  nolesgn2o  27835  nogesgn1o  27837  nodense  27856  nosupbnd2lem1  27879  noinfbnd2lem1  27894  brslts  27955  madebday  28093  negsprop  28228  mulsprop  28323  onsfi  28549  axtgcont1  28737  nb3grpr  29732  dfconngr1  30539  isconngr  30540  1conngr  30545  frgr0v  30613  isplig  30828  isgrpo  30849  isablo  30898  ocval  31632  acunirnmpt  33004  ismbfm  34641  bnj865  35311  bnj1154  35387  bnj1296  35409  bnj1463  35443  r1filimi  35497  wevgblacfn  35595  derangval  35659  dfon2lem3  36275  dfon2lem7  36279  dfrecs2  36442  dfrdg4  36443  isfne  36850  finixpnum  38256  mblfinlem1  38308  mbfresfi  38317  indexdom  38385  heibor1lem  38460  isexid2  38506  ismndo2  38525  rngomndo  38586  pridl  38688  smprngopr  38703  ispridlc  38721  sn-isghm  43405  setindtrs  43752  dford3lem2  43754  dfac11  43789  rp-intrabeq  43948  rp-unirabeq  43949  rp-brsslt  44149  mnuop123d  44972  relpeq4  45656  trfr  45671  permac8prim  45723  fnchoice  45749  axccdom  45938  axccd  45944  stoweidlem31  46745  stoweidlem57  46771  fourierdlem80  46900  fourierdlem103  46923  fourierdlem104  46924  isvonmbl  47352  paireqne  48260  requad2  48388  smprngprmrng  49104  nelsubc3lem  49848  isthinc  50197  0thincg  50236  cnelsubclem  50381  bnd2d  50459