Theorem raleq 3323

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ral 3063  df-rex 3072

This theorem is referenced by:  raleqi  3324  raleqdv  3326  sbralieALT  3356  r19.2zb  4496  inteq  4954  iineq1  5015  friOLD  5638  frsn  5764  fncnv  6622  isoeq4  7317  onminex  7790  tfisg  7843  tfinds  7849  f1oweALT  7959  frxp  8112  frxp2  8130  poseq  8144  frrlem1  8271  frrlem13  8283  wfrlem1OLD  8308  wfrlem15OLD  8323  tfrlem1  8376  tfrlem12  8389  omeulem1  8582  ixpeq1  8902  undifixp  8928  ac6sfi  9287  frfi  9288  iunfi  9340  indexfi  9360  supeq1  9440  supeq2  9443  brttrcl2  9709  ssttrcl  9710  ttrcltr  9711  bnd2  9888  acneq  10038  aceq3lem  10115  dfac5lem4  10121  dfac8  10130  dfac9  10131  kmlem1  10145  kmlem10  10154  kmlem13  10157  cfval  10242  axcc2lem  10431  axcc4dom  10436  axdc3lem3  10447  axdc3lem4  10448  ac4c  10471  ac5  10472  ac6sg  10483  zorn2lem7  10497  xrsupsslem  13286  xrinfmsslem  13287  xrsupss  13288  xrinfmss  13289  fsuppmapnn0fiubex  13957  rexanuz  15292  rexfiuz  15294  modfsummod  15740  gcdcllem3  16442  lcmfval  16558  lcmf0val  16559  lcmfunsnlem  16578  coprmprod  16598  coprmproddvds  16600  isprs  18250  drsdirfi  18258  isdrs2  18259  ispos  18267  pospropd  18280  lubeldm  18306  lubval  18309  glbeldm  18319  glbval  18322  istos  18371  isdlat  18475  mhmpropd  18678  isghm  19092  cntzval  19185  efgval  19585  iscmn  19657  dfrhm2  20253  lidldvgen  20893  ocvval  21220  isobs  21275  coe1fzgsumd  21826  evl1gsumd  21876  mat0dimcrng  21972  mdetunilem9  22122  ist0  22824  cmpcovf  22895  is1stc  22945  2ndc1stc  22955  isref  23013  txflf  23510  ustuqtop4  23749  iscfilu  23793  ispsmet  23810  ismet  23829  isxmet  23830  cncfval  24404  lebnumlem3  24479  fmcfil  24789  iscfil3  24790  caucfil  24800  iscmet3  24810  cfilres  24813  minveclem3  24946  ovolfiniun  25018  finiunmbl  25061  volfiniun  25064  dvcn  25438  ulmval  25892  sltval2  27159  sltres  27165  nolesgn2o  27174  nogesgn1o  27176  nodense  27195  nosupbnd2lem1  27218  noinfbnd2lem1  27233  brsslt  27287  madebday  27394  negsprop  27509  mulsprop  27586  axtgcont1  27719  nb3grpr  28639  dfconngr1  29441  isconngr  29442  1conngr  29447  frgr0v  29515  isplig  29729  isgrpo  29750  isablo  29799  ocval  30533  acunirnmpt  31884  isomnd  32219  isorng  32417  prmidl  32558  ismbfm  33249  bnj865  33934  bnj1154  34010  bnj1296  34032  bnj1463  34066  derangval  34158  setinds  34750  dfon2lem3  34757  dfon2lem7  34761  dfrecs2  34922  dfrdg4  34923  isfne  35224  finixpnum  36473  mblfinlem1  36525  mbfresfi  36534  indexdom  36602  heibor1lem  36677  isexid2  36723  ismndo2  36742  rngomndo  36803  pridl  36905  smprngopr  36920  ispridlc  36938  setindtrs  41764  dford3lem2  41766  dfac11  41804  rp-intrabeq  41970  rp-unirabeq  41971  rp-brsslt  42174  mnuop123d  43021  fnchoice  43713  axccdom  43921  axccd  43928  stoweidlem31  44747  stoweidlem57  44773  fourierdlem80  44902  fourierdlem103  44925  fourierdlem104  44926  isvonmbl  45354  paireqne  46179  requad2  46291  mgmhmpropd  46555  rnghmval  46689  zrrnghm  46716  isthinc  47641  0thincg  47670  bnd2d  47726