Theorem raleq 3286

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   = wceq 1540  ∀wral 3044  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ral 3045  df-rex 3054

This theorem is referenced by:  raleqi  3287  raleqdv  3289  raleleq  3305  sbralieALT  3316  r19.2zb  4447  inteq  4899  iineq1  4959  frsn  5707  fncnv  6555  isoeq4  7257  onminex  7738  tfisg  7787  tfinds  7793  f1oweALT  7907  frxp  8059  frxp2  8077  poseq  8091  frrlem1  8219  frrlem13  8231  tfrlem1  8298  tfrlem12  8311  omeulem1  8500  ixpeq1  8835  undifixp  8861  ac6sfi  9173  frfi  9174  iunfi  9233  indexfi  9250  supeq1  9335  supeq2  9338  brttrcl2  9610  ssttrcl  9611  ttrcltr  9612  bnd2  9789  acneq  9937  aceq3lem  10014  dfac5lem4  10020  dfac5lem4OLD  10022  dfac8  10030  dfac9  10031  kmlem1  10045  kmlem10  10054  kmlem13  10057  cfval  10141  axcc2lem  10330  axcc4dom  10335  axdc3lem3  10346  axdc3lem4  10347  ac4c  10370  ac5  10371  ac6sg  10382  zorn2lem7  10396  xrsupsslem  13209  xrinfmsslem  13210  xrsupss  13211  xrinfmss  13212  fsuppmapnn0fiubex  13899  rexanuz  15253  rexfiuz  15255  modfsummod  15701  gcdcllem3  16412  lcmfval  16532  lcmf0val  16533  lcmfunsnlem  16552  coprmprod  16572  coprmproddvds  16574  isprs  18202  drsdirfi  18211  isdrs2  18212  ispos  18220  pospropd  18231  lubeldm  18257  lubval  18260  glbeldm  18270  glbval  18273  istos  18322  isdlat  18428  mgmhmpropd  18572  mhmpropd  18666  isghm  19094  isghmOLD  19095  cntzval  19200  efgval  19596  iscmn  19668  isomnd  20002  rnghmval  20325  dfrhm2  20359  zrrnghm  20421  isorng  20746  lidldvgen  21241  ocvval  21574  isobs  21627  coe1fzgsumd  22189  evl1gsumd  22242  mat0dimcrng  22355  mdetunilem9  22505  ist0  23205  cmpcovf  23276  is1stc  23326  2ndc1stc  23336  isref  23394  txflf  23891  ustuqtop4  24130  iscfilu  24173  ispsmet  24190  ismet  24209  isxmet  24210  cncfval  24779  lebnumlem3  24860  fmcfil  25170  iscfil3  25171  caucfil  25181  iscmet3  25191  cfilres  25194  minveclem3  25327  ovolfiniun  25400  finiunmbl  25443  volfiniun  25446  dvcn  25821  ulmval  26287  sltval2  27566  sltres  27572  nolesgn2o  27581  nogesgn1o  27583  nodense  27602  nosupbnd2lem1  27625  noinfbnd2lem1  27640  brsslt  27696  madebday  27814  negsprop  27946  mulsprop  28038  onsfi  28252  axtgcont1  28413  nb3grpr  29327  dfconngr1  30132  isconngr  30133  1conngr  30138  frgr0v  30206  isplig  30420  isgrpo  30441  isablo  30490  ocval  31224  acunirnmpt  32602  prmidl  33377  ismbfm  34218  bnj865  34890  bnj1154  34966  bnj1296  34988  bnj1463  35022  wevgblacfn  35086  derangval  35144  setinds  35756  dfon2lem3  35763  dfon2lem7  35767  dfrecs2  35928  dfrdg4  35929  isfne  36317  finixpnum  37589  mblfinlem1  37641  mbfresfi  37650  indexdom  37718  heibor1lem  37793  isexid2  37839  ismndo2  37858  rngomndo  37919  pridl  38021  smprngopr  38036  ispridlc  38054  sn-isghm  42650  setindtrs  43002  dford3lem2  43004  dfac11  43039  rp-intrabeq  43198  rp-unirabeq  43199  rp-brsslt  43400  mnuop123d  44239  relpeq4  44925  trfr  44940  permac8prim  44992  fnchoice  45011  axccdom  45204  axccd  45211  stoweidlem31  46016  stoweidlem57  46042  fourierdlem80  46171  fourierdlem103  46194  fourierdlem104  46195  isvonmbl  46623  paireqne  47499  requad2  47611  nelsubc3lem  49059  isthinc  49408  0thincg  49447  cnelsubclem  49592  bnd2d  49670