Theorem raleq 3295

Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2147, ax-11 2163, and ax-12 2185. (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 3294	. . 3 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∃𝑥 ∈ 𝐵 ¬ 𝜑))
2		rexnal 3090	. . 3 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)
3		rexnal 3090	. . 3 ⊢ (∃𝑥 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐵 𝜑)
4	1, 2, 3	3bitr3g 313	. 2 ⊢ (𝐴 = 𝐵 → (¬ ∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐵 𝜑))
5	4	con4bid 317	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   = wceq 1542  ∀wral 3052  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ral 3053  df-rex 3063

This theorem is referenced by:  raleqi  3296  raleqdv  3298  raleleq  3314  sbralieALT  3325  inteq  4907  iineq1  4966  frsn  5720  fncnv  6573  isoeq4  7276  onminex  7757  tfisg  7806  tfinds  7812  f1oweALT  7926  frxp  8078  frxp2  8096  poseq  8110  frrlem1  8238  frrlem13  8250  tfrlem1  8317  tfrlem12  8330  omeulem1  8519  ixpeq1  8858  undifixp  8884  ac6sfi  9196  frfi  9197  iunfi  9255  indexfi  9272  supeq1  9360  supeq2  9363  brttrcl2  9635  ssttrcl  9636  ttrcltr  9637  setinds  9670  bnd2  9817  acneq  9965  aceq3lem  10042  dfac5lem4  10048  dfac5lem4OLD  10050  dfac8  10058  dfac9  10059  kmlem1  10073  kmlem10  10082  kmlem13  10085  cfval  10169  axcc2lem  10358  axcc4dom  10363  axdc3lem3  10374  axdc3lem4  10375  ac4c  10398  ac5  10399  ac6sg  10410  zorn2lem7  10424  xrsupsslem  13234  xrinfmsslem  13235  xrsupss  13236  xrinfmss  13237  fsuppmapnn0fiubex  13927  rexanuz  15281  rexfiuz  15283  modfsummod  15729  gcdcllem3  16440  lcmfval  16560  lcmf0val  16561  lcmfunsnlem  16580  coprmprod  16600  coprmproddvds  16602  isprs  18231  drsdirfi  18240  isdrs2  18241  ispos  18249  pospropd  18260  lubeldm  18286  lubval  18289  glbeldm  18299  glbval  18302  istos  18351  isdlat  18457  mgmhmpropd  18635  mhmpropd  18729  isghm  19156  isghmOLD  19157  cntzval  19262  efgval  19658  iscmn  19730  isomnd  20064  rnghmval  20388  dfrhm2  20422  zrrnghm  20481  isorng  20806  lidldvgen  21301  ocvval  21634  isobs  21687  coe1fzgsumd  22260  evl1gsumd  22313  mat0dimcrng  22426  mdetunilem9  22576  ist0  23276  cmpcovf  23347  is1stc  23397  2ndc1stc  23407  isref  23465  txflf  23962  ustuqtop4  24200  iscfilu  24243  ispsmet  24260  ismet  24279  isxmet  24280  cncfval  24849  lebnumlem3  24930  fmcfil  25240  iscfil3  25241  caucfil  25251  iscmet3  25261  cfilres  25264  minveclem3  25397  ovolfiniun  25470  finiunmbl  25513  volfiniun  25516  dvcn  25891  ulmval  26357  ltsval2  27636  ltsres  27642  nolesgn2o  27651  nogesgn1o  27653  nodense  27672  nosupbnd2lem1  27695  noinfbnd2lem1  27710  brslts  27770  madebday  27908  negsprop  28043  mulsprop  28138  onsfi  28364  axtgcont1  28552  nb3grpr  29467  dfconngr1  30275  isconngr  30276  1conngr  30281  frgr0v  30349  isplig  30564  isgrpo  30585  isablo  30634  ocval  31368  acunirnmpt  32749  prmidl  33533  ismbfm  34429  bnj865  35099  bnj1154  35175  bnj1296  35197  bnj1463  35231  r1filimi  35280  wevgblacfn  35325  derangval  35383  dfon2lem3  35999  dfon2lem7  36003  dfrecs2  36166  dfrdg4  36167  isfne  36555  finixpnum  37856  mblfinlem1  37908  mbfresfi  37917  indexdom  37985  heibor1lem  38060  isexid2  38106  ismndo2  38125  rngomndo  38186  pridl  38288  smprngopr  38303  ispridlc  38321  sn-isghm  43031  setindtrs  43382  dford3lem2  43384  dfac11  43419  rp-intrabeq  43578  rp-unirabeq  43579  rp-brsslt  43779  mnuop123d  44618  relpeq4  45303  trfr  45318  permac8prim  45370  fnchoice  45389  axccdom  45580  axccd  45587  stoweidlem31  46389  stoweidlem57  46415  fourierdlem80  46544  fourierdlem103  46567  fourierdlem104  46568  isvonmbl  46996  paireqne  47871  requad2  47983  nelsubc3lem  49429  isthinc  49778  0thincg  49817  cnelsubclem  49962  bnd2d  50040