Theorem raleq 3293

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   = wceq 1541  ∀wral 3051  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ral 3052  df-rex 3061

This theorem is referenced by:  raleqi  3294  raleqdv  3296  raleleq  3312  sbralieALT  3323  inteq  4905  iineq1  4964  frsn  5712  fncnv  6565  isoeq4  7266  onminex  7747  tfisg  7796  tfinds  7802  f1oweALT  7916  frxp  8068  frxp2  8086  poseq  8100  frrlem1  8228  frrlem13  8240  tfrlem1  8307  tfrlem12  8320  omeulem1  8509  ixpeq1  8846  undifixp  8872  ac6sfi  9184  frfi  9185  iunfi  9243  indexfi  9260  supeq1  9348  supeq2  9351  brttrcl2  9623  ssttrcl  9624  ttrcltr  9625  setinds  9658  bnd2  9805  acneq  9953  aceq3lem  10030  dfac5lem4  10036  dfac5lem4OLD  10038  dfac8  10046  dfac9  10047  kmlem1  10061  kmlem10  10070  kmlem13  10073  cfval  10157  axcc2lem  10346  axcc4dom  10351  axdc3lem3  10362  axdc3lem4  10363  ac4c  10386  ac5  10387  ac6sg  10398  zorn2lem7  10412  xrsupsslem  13222  xrinfmsslem  13223  xrsupss  13224  xrinfmss  13225  fsuppmapnn0fiubex  13915  rexanuz  15269  rexfiuz  15271  modfsummod  15717  gcdcllem3  16428  lcmfval  16548  lcmf0val  16549  lcmfunsnlem  16568  coprmprod  16588  coprmproddvds  16590  isprs  18219  drsdirfi  18228  isdrs2  18229  ispos  18237  pospropd  18248  lubeldm  18274  lubval  18277  glbeldm  18287  glbval  18290  istos  18339  isdlat  18445  mgmhmpropd  18623  mhmpropd  18717  isghm  19144  isghmOLD  19145  cntzval  19250  efgval  19646  iscmn  19718  isomnd  20052  rnghmval  20376  dfrhm2  20410  zrrnghm  20469  isorng  20794  lidldvgen  21289  ocvval  21622  isobs  21675  coe1fzgsumd  22248  evl1gsumd  22301  mat0dimcrng  22414  mdetunilem9  22564  ist0  23264  cmpcovf  23335  is1stc  23385  2ndc1stc  23395  isref  23453  txflf  23950  ustuqtop4  24188  iscfilu  24231  ispsmet  24248  ismet  24267  isxmet  24268  cncfval  24837  lebnumlem3  24918  fmcfil  25228  iscfil3  25229  caucfil  25239  iscmet3  25249  cfilres  25252  minveclem3  25385  ovolfiniun  25458  finiunmbl  25501  volfiniun  25504  dvcn  25879  ulmval  26345  ltsval2  27624  ltsres  27630  nolesgn2o  27639  nogesgn1o  27641  nodense  27660  nosupbnd2lem1  27683  noinfbnd2lem1  27698  brslts  27758  madebday  27896  negsprop  28031  mulsprop  28126  onsfi  28352  axtgcont1  28540  nb3grpr  29455  dfconngr1  30263  isconngr  30264  1conngr  30269  frgr0v  30337  isplig  30551  isgrpo  30572  isablo  30621  ocval  31355  acunirnmpt  32737  prmidl  33521  ismbfm  34408  bnj865  35079  bnj1154  35155  bnj1296  35177  bnj1463  35211  r1filimi  35259  wevgblacfn  35303  derangval  35361  dfon2lem3  35977  dfon2lem7  35981  dfrecs2  36144  dfrdg4  36145  isfne  36533  finixpnum  37806  mblfinlem1  37858  mbfresfi  37867  indexdom  37935  heibor1lem  38010  isexid2  38056  ismndo2  38075  rngomndo  38136  pridl  38238  smprngopr  38253  ispridlc  38271  sn-isghm  42916  setindtrs  43267  dford3lem2  43269  dfac11  43304  rp-intrabeq  43463  rp-unirabeq  43464  rp-brsslt  43664  mnuop123d  44503  relpeq4  45188  trfr  45203  permac8prim  45255  fnchoice  45274  axccdom  45466  axccd  45473  stoweidlem31  46275  stoweidlem57  46301  fourierdlem80  46430  fourierdlem103  46453  fourierdlem104  46454  isvonmbl  46882  paireqne  47757  requad2  47869  nelsubc3lem  49315  isthinc  49664  0thincg  49703  cnelsubclem  49848  bnd2d  49926