Theorem raleq 3316

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 3315	. . 3 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∃𝑥 ∈ 𝐵 ¬ 𝜑))
2		rexnal 3114	. . 3 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)
3		rexnal 3114	. . 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 3076  ∃wrex 3086

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ral 3077  df-rex 3087

This theorem is used by:  raleqi  3317  raleqdv  3319  raleleq  3331  sbralieALT  3339  inteq  4910  iineq1  4969  frsn  5743  fncnv  6607  isoeq4  7322  onminex  7802  tfisg  7851  tfinds  7857  f1oweALT  7970  frxp  8125  frxp2  8143  poseq  8157  frrlem1  8286  frrlem13  8298  tfrlem1  8365  tfrlem12  8379  omeulem1  8570  ixpeq1  8916  undifixp  8942  ac6sfi  9255  frfi  9256  iunfi  9311  indexfi  9328  supeq1  9416  supeq2  9419  brttrcl2  9694  ssttrcl  9695  ttrcltr  9696  setinds  9729  bnd2  9896  acneq  10047  aceq3lem  10124  dfac5lem4  10130  dfac8  10139  dfac9  10140  kmlem1  10154  kmlem10  10163  kmlem13  10166  cfval  10249  axcc2lem  10439  axcc4dom  10444  axdc3lem3  10455  axdc3lem4  10456  ac4c  10479  ac5  10480  ac6sg  10491  zorn2lem7  10505  xrsupsslem  13360  xrinfmsslem  13361  xrsupss  13362  xrinfmss  13363  fsuppmapnn0fiubex  14057  rexanuz  15434  rexfiuz  15436  modfsummod  15882  gcdcllem3  16592  lcmfval  16712  lcmf0val  16713  lcmfunsnlem  16732  coprmprod  16752  coprmproddvds  16754  isprs  18385  drsdirfi  18394  isdrs2  18395  ispos  18403  pospropd  18414  lubeldm  18440  lubval  18443  glbeldm  18453  glbval  18456  istos  18505  isdlat  18611  idressidex  18775  mgmhmpropd  18801  mhmpropd  18901  isghm  19344  cntzval  19449  efgval  19845  iscmn  19917  isomnd  20251  rnghmval  20582  dfrhm2  20616  rhmval0  20617  zrrnghm  20699  isorng  21028  prmidl  21529  lidldvgen  21566  ocvval  21881  isobs  21934  coe1fzgsumd  22530  evl1gsumd  22583  mat0dimcrng  22693  mdetunilem9  22843  ist0  23546  cmpcovf  23617  is1stc  23667  2ndc1stc  23677  isref  23736  txflf  24233  ustuqtop4  24471  iscfilu  24514  ispsmet  24531  ismet  24550  isxmet  24551  cncfval  25117  lebnumlem3  25192  fmcfil  25501  iscfil3  25502  caucfil  25512  iscmet3  25522  cfilres  25525  minveclem3  25658  ovolfiniun  25730  finiunmbl  25773  volfiniun  25776  dvcn  26149  ulmval  26617  ltsval2  27893  ltsres  27899  nolesgn2o  27908  nogesgn1o  27910  nodense  27929  nosupbnd2lem1  27952  noinfbnd2lem1  27967  brslts  28028  madebday  28166  negsprop  28301  mulsprop  28396  onsfi  28622  axtgcont1  28810  nb3grpr  29843  dfconngr1  30669  isconngr  30670  1conngr  30675  frgr0v  30743  isplig  30958  isgrpo  30979  isablo  31028  ocval  31762  acunirnmpt  33133  ismbfm  34763  bnj865  35433  bnj1154  35509  bnj1296  35531  bnj1463  35565  r1filimi  35612  wevgblacfn  35709  derangval  35747  dfon2lem3  36363  dfon2lem7  36367  dfrecs2  36530  dfrdg4  36531  isfne  36959  finixpnum  38360  mblfinlem1  38407  mbfresfi  38416  indexdom  38485  heibor1lem  38560  isexid2  38606  ismndo2  38625  rngomndo  38686  pridl  38788  smprngopr  38803  ispridlc  38821  sn-isghm  43520  setindtrs  43867  dford3lem2  43869  dfac11  43904  rp-intrabeq  44063  rp-unirabeq  44064  rp-brsslt  44264  mnuop123d  45087  relpeq4  45771  trfr  45786  permac8prim  45838  fnchoice  45864  axccdom  46053  axccd  46059  stoweidlem31  46860  stoweidlem57  46886  fourierdlem80  47015  fourierdlem103  47038  fourierdlem104  47039  isvonmbl  47467  paireqne  48412  requad2  48540  smprngprmrng  49255  nelsubc3lem  49997  isthinc  50346  0thincg  50385  cnelsubclem  50530  bnd2d  50608