Theorem raleq 3289

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

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

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 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ral 3048  df-rex 3057

This theorem is referenced by:  raleqi  3290  raleqdv  3292  raleleq  3308  sbralieALT  3319  r19.2zb  4443  inteq  4898  iineq1  4957  frsn  5702  fncnv  6554  isoeq4  7254  onminex  7735  tfisg  7784  tfinds  7790  f1oweALT  7904  frxp  8056  frxp2  8074  poseq  8088  frrlem1  8216  frrlem13  8228  tfrlem1  8295  tfrlem12  8308  omeulem1  8497  ixpeq1  8832  undifixp  8858  ac6sfi  9168  frfi  9169  iunfi  9227  indexfi  9244  supeq1  9329  supeq2  9332  brttrcl2  9604  ssttrcl  9605  ttrcltr  9606  setinds  9639  bnd2  9786  acneq  9934  aceq3lem  10011  dfac5lem4  10017  dfac5lem4OLD  10019  dfac8  10027  dfac9  10028  kmlem1  10042  kmlem10  10051  kmlem13  10054  cfval  10138  axcc2lem  10327  axcc4dom  10332  axdc3lem3  10343  axdc3lem4  10344  ac4c  10367  ac5  10368  ac6sg  10379  zorn2lem7  10393  xrsupsslem  13206  xrinfmsslem  13207  xrsupss  13208  xrinfmss  13209  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  18606  mhmpropd  18700  isghm  19127  isghmOLD  19128  cntzval  19233  efgval  19629  iscmn  19701  isomnd  20035  rnghmval  20358  dfrhm2  20392  zrrnghm  20451  isorng  20776  lidldvgen  21271  ocvval  21604  isobs  21657  coe1fzgsumd  22219  evl1gsumd  22272  mat0dimcrng  22385  mdetunilem9  22535  ist0  23235  cmpcovf  23306  is1stc  23356  2ndc1stc  23366  isref  23424  txflf  23921  ustuqtop4  24159  iscfilu  24202  ispsmet  24219  ismet  24238  isxmet  24239  cncfval  24808  lebnumlem3  24889  fmcfil  25199  iscfil3  25200  caucfil  25210  iscmet3  25220  cfilres  25223  minveclem3  25356  ovolfiniun  25429  finiunmbl  25472  volfiniun  25475  dvcn  25850  ulmval  26316  sltval2  27595  sltres  27601  nolesgn2o  27610  nogesgn1o  27612  nodense  27631  nosupbnd2lem1  27654  noinfbnd2lem1  27669  brsslt  27725  madebday  27845  negsprop  27977  mulsprop  28069  onsfi  28283  axtgcont1  28446  nb3grpr  29360  dfconngr1  30168  isconngr  30169  1conngr  30174  frgr0v  30242  isplig  30456  isgrpo  30477  isablo  30526  ocval  31260  acunirnmpt  32641  prmidl  33405  ismbfm  34264  bnj865  34935  bnj1154  35011  bnj1296  35033  bnj1463  35067  r1filimi  35114  wevgblacfn  35153  derangval  35211  dfon2lem3  35827  dfon2lem7  35831  dfrecs2  35994  dfrdg4  35995  isfne  36383  finixpnum  37655  mblfinlem1  37707  mbfresfi  37716  indexdom  37784  heibor1lem  37859  isexid2  37905  ismndo2  37924  rngomndo  37985  pridl  38087  smprngopr  38102  ispridlc  38120  sn-isghm  42776  setindtrs  43128  dford3lem2  43130  dfac11  43165  rp-intrabeq  43324  rp-unirabeq  43325  rp-brsslt  43526  mnuop123d  44365  relpeq4  45050  trfr  45065  permac8prim  45117  fnchoice  45136  axccdom  45329  axccd  45336  stoweidlem31  46139  stoweidlem57  46165  fourierdlem80  46294  fourierdlem103  46317  fourierdlem104  46318  isvonmbl  46746  paireqne  47621  requad2  47733  nelsubc3lem  49181  isthinc  49530  0thincg  49569  cnelsubclem  49714  bnd2d  49792