Theorem raleq 3320

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   = wceq 1536  ∀wral 3058  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ral 3059  df-rex 3068

This theorem is referenced by:  raleqi  3321  raleqdv  3323  raleleq  3339  sbralieALT  3356  r19.2zb  4501  inteq  4953  iineq1  5013  friOLD  5646  frsn  5775  fncnv  6640  isoeq4  7339  onminex  7821  tfisg  7874  tfinds  7880  f1oweALT  7995  frxp  8149  frxp2  8167  poseq  8181  frrlem1  8309  frrlem13  8321  wfrlem1OLD  8346  wfrlem15OLD  8361  tfrlem1  8414  tfrlem12  8427  omeulem1  8618  ixpeq1  8946  undifixp  8972  ac6sfi  9317  frfi  9318  iunfi  9380  indexfi  9397  supeq1  9482  supeq2  9485  brttrcl2  9751  ssttrcl  9752  ttrcltr  9753  bnd2  9930  acneq  10080  aceq3lem  10157  dfac5lem4  10163  dfac5lem4OLD  10165  dfac8  10173  dfac9  10174  kmlem1  10188  kmlem10  10197  kmlem13  10200  cfval  10284  axcc2lem  10473  axcc4dom  10478  axdc3lem3  10489  axdc3lem4  10490  ac4c  10513  ac5  10514  ac6sg  10525  zorn2lem7  10539  xrsupsslem  13345  xrinfmsslem  13346  xrsupss  13347  xrinfmss  13348  fsuppmapnn0fiubex  14029  rexanuz  15380  rexfiuz  15382  modfsummod  15826  gcdcllem3  16534  lcmfval  16654  lcmf0val  16655  lcmfunsnlem  16674  coprmprod  16694  coprmproddvds  16696  isprs  18353  drsdirfi  18362  isdrs2  18363  ispos  18371  pospropd  18384  lubeldm  18410  lubval  18413  glbeldm  18423  glbval  18426  istos  18475  isdlat  18579  mgmhmpropd  18723  mhmpropd  18817  isghm  19245  isghmOLD  19246  cntzval  19351  efgval  19749  iscmn  19821  rnghmval  20456  dfrhm2  20490  zrrnghm  20552  lidldvgen  21361  ocvval  21702  isobs  21757  coe1fzgsumd  22323  evl1gsumd  22376  mat0dimcrng  22491  mdetunilem9  22641  ist0  23343  cmpcovf  23414  is1stc  23464  2ndc1stc  23474  isref  23532  txflf  24029  ustuqtop4  24268  iscfilu  24312  ispsmet  24329  ismet  24348  isxmet  24349  cncfval  24927  lebnumlem3  25008  fmcfil  25319  iscfil3  25320  caucfil  25330  iscmet3  25340  cfilres  25343  minveclem3  25476  ovolfiniun  25549  finiunmbl  25592  volfiniun  25595  dvcn  25971  ulmval  26437  sltval2  27715  sltres  27721  nolesgn2o  27730  nogesgn1o  27732  nodense  27751  nosupbnd2lem1  27774  noinfbnd2lem1  27789  brsslt  27844  madebday  27952  negsprop  28081  mulsprop  28170  axtgcont1  28490  nb3grpr  29413  dfconngr1  30216  isconngr  30217  1conngr  30222  frgr0v  30290  isplig  30504  isgrpo  30525  isablo  30574  ocval  31308  acunirnmpt  32675  isomnd  33060  isorng  33308  prmidl  33447  ismbfm  34231  bnj865  34915  bnj1154  34991  bnj1296  35013  bnj1463  35047  wevgblacfn  35092  derangval  35151  setinds  35759  dfon2lem3  35766  dfon2lem7  35770  dfrecs2  35931  dfrdg4  35932  isfne  36321  finixpnum  37591  mblfinlem1  37643  mbfresfi  37652  indexdom  37720  heibor1lem  37795  isexid2  37841  ismndo2  37860  rngomndo  37921  pridl  38023  smprngopr  38038  ispridlc  38056  sn-isghm  42659  setindtrs  43013  dford3lem2  43015  dfac11  43050  rp-intrabeq  43209  rp-unirabeq  43210  rp-brsslt  43412  mnuop123d  44257  fnchoice  44966  axccdom  45164  axccd  45171  stoweidlem31  45986  stoweidlem57  46012  fourierdlem80  46141  fourierdlem103  46164  fourierdlem104  46165  isvonmbl  46593  paireqne  47435  requad2  47547  isthinc  48820  0thincg  48850  bnd2d  48911