Theorem raleq 3302

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

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

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  raleqi  3303  raleqdv  3305  raleleq  3321  sbralieALT  3338  r19.2zb  4471  inteq  4925  iineq1  4985  friOLD  5612  frsn  5742  fncnv  6608  isoeq4  7312  onminex  7794  tfisg  7847  tfinds  7853  f1oweALT  7969  frxp  8123  frxp2  8141  poseq  8155  frrlem1  8283  frrlem13  8295  wfrlem1OLD  8320  wfrlem15OLD  8335  tfrlem1  8388  tfrlem12  8401  omeulem1  8592  ixpeq1  8920  undifixp  8946  ac6sfi  9290  frfi  9291  iunfi  9353  indexfi  9370  supeq1  9455  supeq2  9458  brttrcl2  9726  ssttrcl  9727  ttrcltr  9728  bnd2  9905  acneq  10055  aceq3lem  10132  dfac5lem4  10138  dfac5lem4OLD  10140  dfac8  10148  dfac9  10149  kmlem1  10163  kmlem10  10172  kmlem13  10175  cfval  10259  axcc2lem  10448  axcc4dom  10453  axdc3lem3  10464  axdc3lem4  10465  ac4c  10488  ac5  10489  ac6sg  10500  zorn2lem7  10514  xrsupsslem  13321  xrinfmsslem  13322  xrsupss  13323  xrinfmss  13324  fsuppmapnn0fiubex  14008  rexanuz  15362  rexfiuz  15364  modfsummod  15808  gcdcllem3  16518  lcmfval  16638  lcmf0val  16639  lcmfunsnlem  16658  coprmprod  16678  coprmproddvds  16680  isprs  18306  drsdirfi  18315  isdrs2  18316  ispos  18324  pospropd  18335  lubeldm  18361  lubval  18364  glbeldm  18374  glbval  18377  istos  18426  isdlat  18530  mgmhmpropd  18674  mhmpropd  18768  isghm  19196  isghmOLD  19197  cntzval  19302  efgval  19696  iscmn  19768  rnghmval  20398  dfrhm2  20432  zrrnghm  20494  lidldvgen  21293  ocvval  21625  isobs  21678  coe1fzgsumd  22240  evl1gsumd  22293  mat0dimcrng  22406  mdetunilem9  22556  ist0  23256  cmpcovf  23327  is1stc  23377  2ndc1stc  23387  isref  23445  txflf  23942  ustuqtop4  24181  iscfilu  24224  ispsmet  24241  ismet  24260  isxmet  24261  cncfval  24830  lebnumlem3  24911  fmcfil  25222  iscfil3  25223  caucfil  25233  iscmet3  25243  cfilres  25246  minveclem3  25379  ovolfiniun  25452  finiunmbl  25495  volfiniun  25498  dvcn  25873  ulmval  26339  sltval2  27618  sltres  27624  nolesgn2o  27633  nogesgn1o  27635  nodense  27654  nosupbnd2lem1  27677  noinfbnd2lem1  27692  brsslt  27747  madebday  27855  negsprop  27984  mulsprop  28073  axtgcont1  28393  nb3grpr  29307  dfconngr1  30115  isconngr  30116  1conngr  30121  frgr0v  30189  isplig  30403  isgrpo  30424  isablo  30473  ocval  31207  acunirnmpt  32583  isomnd  33015  isorng  33267  prmidl  33401  ismbfm  34228  bnj865  34900  bnj1154  34976  bnj1296  34998  bnj1463  35032  wevgblacfn  35077  derangval  35135  setinds  35742  dfon2lem3  35749  dfon2lem7  35753  dfrecs2  35914  dfrdg4  35915  isfne  36303  finixpnum  37575  mblfinlem1  37627  mbfresfi  37636  indexdom  37704  heibor1lem  37779  isexid2  37825  ismndo2  37844  rngomndo  37905  pridl  38007  smprngopr  38022  ispridlc  38040  sn-isghm  42643  setindtrs  42996  dford3lem2  42998  dfac11  43033  rp-intrabeq  43192  rp-unirabeq  43193  rp-brsslt  43394  mnuop123d  44234  relpeq4  44920  trfr  44935  fnchoice  45001  axccdom  45194  axccd  45201  stoweidlem31  46008  stoweidlem57  46034  fourierdlem80  46163  fourierdlem103  46186  fourierdlem104  46187  isvonmbl  46615  paireqne  47473  requad2  47585  nelsubc3lem  48985  isthinc  49253  0thincg  49292  cnelsubclem  49428  bnd2d  49493