Theorem raleq 3293

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 3292	. . 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  3294  raleqdv  3296  raleleq  3308  sbralieALT  3317  inteq  4893  iineq1  4952  frsn  5713  fncnv  6566  isoeq4  7269  onminex  7750  tfisg  7799  tfinds  7805  f1oweALT  7919  frxp  8070  frxp2  8088  poseq  8102  frrlem1  8230  frrlem13  8242  tfrlem1  8309  tfrlem12  8322  omeulem1  8511  ixpeq1  8850  undifixp  8876  ac6sfi  9188  frfi  9189  iunfi  9247  indexfi  9264  supeq1  9352  supeq2  9355  brttrcl2  9629  ssttrcl  9630  ttrcltr  9631  setinds  9664  bnd2  9811  acneq  9959  aceq3lem  10036  dfac5lem4  10042  dfac5lem4OLD  10044  dfac8  10052  dfac9  10053  kmlem1  10067  kmlem10  10076  kmlem13  10079  cfval  10163  axcc2lem  10352  axcc4dom  10357  axdc3lem3  10368  axdc3lem4  10369  ac4c  10392  ac5  10393  ac6sg  10404  zorn2lem7  10418  xrsupsslem  13253  xrinfmsslem  13254  xrsupss  13255  xrinfmss  13256  fsuppmapnn0fiubex  13948  rexanuz  15302  rexfiuz  15304  modfsummod  15751  gcdcllem3  16464  lcmfval  16584  lcmf0val  16585  lcmfunsnlem  16604  coprmprod  16624  coprmproddvds  16626  isprs  18256  drsdirfi  18265  isdrs2  18266  ispos  18274  pospropd  18285  lubeldm  18311  lubval  18314  glbeldm  18324  glbval  18327  istos  18376  isdlat  18482  mgmhmpropd  18660  mhmpropd  18754  isghm  19184  isghmOLD  19185  cntzval  19290  efgval  19686  iscmn  19758  isomnd  20092  rnghmval  20414  dfrhm2  20448  zrrnghm  20507  isorng  20832  lidldvgen  21327  ocvval  21660  isobs  21713  coe1fzgsumd  22282  evl1gsumd  22335  mat0dimcrng  22448  mdetunilem9  22598  ist0  23298  cmpcovf  23369  is1stc  23419  2ndc1stc  23429  isref  23487  txflf  23984  ustuqtop4  24222  iscfilu  24265  ispsmet  24282  ismet  24301  isxmet  24302  cncfval  24868  lebnumlem3  24943  fmcfil  25252  iscfil3  25253  caucfil  25263  iscmet3  25273  cfilres  25276  minveclem3  25409  ovolfiniun  25481  finiunmbl  25524  volfiniun  25527  dvcn  25901  ulmval  26361  ltsval2  27637  ltsres  27643  nolesgn2o  27652  nogesgn1o  27654  nodense  27673  nosupbnd2lem1  27696  noinfbnd2lem1  27711  brslts  27771  madebday  27909  negsprop  28044  mulsprop  28139  onsfi  28365  axtgcont1  28553  nb3grpr  29468  dfconngr1  30276  isconngr  30277  1conngr  30282  frgr0v  30350  isplig  30565  isgrpo  30586  isablo  30635  ocval  31369  acunirnmpt  32750  prmidl  33518  ismbfm  34414  bnj865  35084  bnj1154  35160  bnj1296  35182  bnj1463  35216  r1filimi  35265  wevgblacfn  35310  derangval  35368  dfon2lem3  35984  dfon2lem7  35988  dfrecs2  36151  dfrdg4  36152  isfne  36540  finixpnum  37943  mblfinlem1  37995  mbfresfi  38004  indexdom  38072  heibor1lem  38147  isexid2  38193  ismndo2  38212  rngomndo  38273  pridl  38375  smprngopr  38390  ispridlc  38408  sn-isghm  43123  setindtrs  43474  dford3lem2  43476  dfac11  43511  rp-intrabeq  43670  rp-unirabeq  43671  rp-brsslt  43871  mnuop123d  44710  relpeq4  45395  trfr  45410  permac8prim  45462  fnchoice  45481  axccdom  45672  axccd  45679  stoweidlem31  46480  stoweidlem57  46506  fourierdlem80  46635  fourierdlem103  46658  fourierdlem104  46659  isvonmbl  47087  paireqne  47986  requad2  48114  nelsubc3lem  49560  isthinc  49909  0thincg  49948  cnelsubclem  50093  bnd2d  50171