Theorem raleq 3322

Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2179, ax-11 2195, and ax-12 2216. (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 3321	. . 3 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∃𝑥 ∈ 𝐵 ¬ 𝜑))
2		rexnal 3119	. . 3 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)
3		rexnal 3119	. . 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 3081  ∃wrex 3091

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 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ral 3082  df-rex 3092

This theorem is used by:  raleqi  3323  raleqdv  3325  raleleq  3337  sbralieALT  3345  inteq  4917  iineq1  4976  frsn  5751  fncnv  6613  isoeq4  7327  onminex  7807  tfisg  7856  tfinds  7862  f1oweALT  7975  frxp  8128  frxp2  8146  poseq  8160  frrlem1  8289  frrlem13  8301  tfrlem1  8368  tfrlem12  8382  omeulem1  8573  ixpeq1  8912  undifixp  8938  ac6sfi  9251  frfi  9252  iunfi  9307  indexfi  9324  supeq1  9412  supeq2  9415  brttrcl2  9690  ssttrcl  9691  ttrcltr  9692  setinds  9725  bnd2  9892  acneq  10043  aceq3lem  10120  dfac5lem4  10126  dfac8  10135  dfac9  10136  kmlem1  10150  kmlem10  10159  kmlem13  10162  cfval  10245  axcc2lem  10435  axcc4dom  10440  axdc3lem3  10451  axdc3lem4  10452  ac4c  10475  ac5  10476  ac6sg  10487  zorn2lem7  10501  xrsupsslem  13349  xrinfmsslem  13350  xrsupss  13351  xrinfmss  13352  fsuppmapnn0fiubex  14046  rexanuz  15421  rexfiuz  15423  modfsummod  15869  gcdcllem3  16581  lcmfval  16701  lcmf0val  16702  lcmfunsnlem  16721  coprmprod  16741  coprmproddvds  16743  isprs  18374  drsdirfi  18383  isdrs2  18384  ispos  18392  pospropd  18403  lubeldm  18429  lubval  18432  glbeldm  18442  glbval  18445  istos  18494  isdlat  18600  idressidex  18764  mgmhmpropd  18788  mhmpropd  18887  isghm  19330  cntzval  19435  efgval  19831  iscmn  19903  isomnd  20237  rnghmval  20568  dfrhm2  20602  rhmval0  20603  zrrnghm  20685  isorng  21014  prmidl  21515  lidldvgen  21552  ocvval  21867  isobs  21920  coe1fzgsumd  22514  evl1gsumd  22567  mat0dimcrng  22677  mdetunilem9  22827  ist0  23527  cmpcovf  23598  is1stc  23648  2ndc1stc  23658  isref  23717  txflf  24214  ustuqtop4  24452  iscfilu  24495  ispsmet  24512  ismet  24531  isxmet  24532  cncfval  25098  lebnumlem3  25173  fmcfil  25482  iscfil3  25483  caucfil  25493  iscmet3  25503  cfilres  25506  minveclem3  25639  ovolfiniun  25711  finiunmbl  25754  volfiniun  25757  dvcn  26131  ulmval  26594  ltsval2  27871  ltsres  27877  nolesgn2o  27886  nogesgn1o  27888  nodense  27907  nosupbnd2lem1  27930  noinfbnd2lem1  27945  brslts  28006  madebday  28144  negsprop  28279  mulsprop  28374  onsfi  28600  axtgcont1  28788  nb3grpr  29790  dfconngr1  30610  isconngr  30611  1conngr  30616  frgr0v  30684  isplig  30899  isgrpo  30920  isablo  30969  ocval  31703  acunirnmpt  33075  ismbfm  34706  bnj865  35376  bnj1154  35452  bnj1296  35474  bnj1463  35508  r1filimi  35555  wevgblacfn  35652  derangval  35696  dfon2lem3  36312  dfon2lem7  36316  dfrecs2  36479  dfrdg4  36480  isfne  36907  finixpnum  38313  mblfinlem1  38365  mbfresfi  38374  indexdom  38443  heibor1lem  38518  isexid2  38564  ismndo2  38583  rngomndo  38644  pridl  38746  smprngopr  38761  ispridlc  38779  sn-isghm  43463  setindtrs  43810  dford3lem2  43812  dfac11  43847  rp-intrabeq  44006  rp-unirabeq  44007  rp-brsslt  44207  mnuop123d  45030  relpeq4  45714  trfr  45729  permac8prim  45781  fnchoice  45807  axccdom  45996  axccd  46002  stoweidlem31  46803  stoweidlem57  46829  fourierdlem80  46958  fourierdlem103  46981  fourierdlem104  46982  isvonmbl  47410  paireqne  48318  requad2  48446  smprngprmrng  49161  nelsubc3lem  49905  isthinc  50254  0thincg  50293  cnelsubclem  50438  bnd2d  50516