Theorem raleq 3331

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ral 3068  df-rex 3077

This theorem is referenced by:  raleqi  3332  raleqdv  3334  raleleq  3350  sbralieALT  3367  r19.2zb  4519  inteq  4973  iineq1  5032  friOLD  5658  frsn  5787  fncnv  6651  isoeq4  7356  onminex  7838  tfisg  7891  tfinds  7897  f1oweALT  8013  frxp  8167  frxp2  8185  poseq  8199  frrlem1  8327  frrlem13  8339  wfrlem1OLD  8364  wfrlem15OLD  8379  tfrlem1  8432  tfrlem12  8445  omeulem1  8638  ixpeq1  8966  undifixp  8992  ac6sfi  9348  frfi  9349  iunfi  9411  indexfi  9430  supeq1  9514  supeq2  9517  brttrcl2  9783  ssttrcl  9784  ttrcltr  9785  bnd2  9962  acneq  10112  aceq3lem  10189  dfac5lem4  10195  dfac5lem4OLD  10197  dfac8  10205  dfac9  10206  kmlem1  10220  kmlem10  10229  kmlem13  10232  cfval  10316  axcc2lem  10505  axcc4dom  10510  axdc3lem3  10521  axdc3lem4  10522  ac4c  10545  ac5  10546  ac6sg  10557  zorn2lem7  10571  xrsupsslem  13369  xrinfmsslem  13370  xrsupss  13371  xrinfmss  13372  fsuppmapnn0fiubex  14043  rexanuz  15394  rexfiuz  15396  modfsummod  15842  gcdcllem3  16547  lcmfval  16668  lcmf0val  16669  lcmfunsnlem  16688  coprmprod  16708  coprmproddvds  16710  isprs  18367  drsdirfi  18375  isdrs2  18376  ispos  18384  pospropd  18397  lubeldm  18423  lubval  18426  glbeldm  18436  glbval  18439  istos  18488  isdlat  18592  mgmhmpropd  18736  mhmpropd  18827  isghm  19255  isghmOLD  19256  cntzval  19361  efgval  19759  iscmn  19831  rnghmval  20466  dfrhm2  20500  zrrnghm  20562  lidldvgen  21367  ocvval  21708  isobs  21763  coe1fzgsumd  22329  evl1gsumd  22382  mat0dimcrng  22497  mdetunilem9  22647  ist0  23349  cmpcovf  23420  is1stc  23470  2ndc1stc  23480  isref  23538  txflf  24035  ustuqtop4  24274  iscfilu  24318  ispsmet  24335  ismet  24354  isxmet  24355  cncfval  24933  lebnumlem3  25014  fmcfil  25325  iscfil3  25326  caucfil  25336  iscmet3  25346  cfilres  25349  minveclem3  25482  ovolfiniun  25555  finiunmbl  25598  volfiniun  25601  dvcn  25977  ulmval  26441  sltval2  27719  sltres  27725  nolesgn2o  27734  nogesgn1o  27736  nodense  27755  nosupbnd2lem1  27778  noinfbnd2lem1  27793  brsslt  27848  madebday  27956  negsprop  28085  mulsprop  28174  axtgcont1  28494  nb3grpr  29417  dfconngr1  30220  isconngr  30221  1conngr  30226  frgr0v  30294  isplig  30508  isgrpo  30529  isablo  30578  ocval  31312  acunirnmpt  32677  isomnd  33051  isorng  33294  prmidl  33433  ismbfm  34215  bnj865  34899  bnj1154  34975  bnj1296  34997  bnj1463  35031  wevgblacfn  35076  derangval  35135  setinds  35742  dfon2lem3  35749  dfon2lem7  35753  dfrecs2  35914  dfrdg4  35915  isfne  36305  finixpnum  37565  mblfinlem1  37617  mbfresfi  37626  indexdom  37694  heibor1lem  37769  isexid2  37815  ismndo2  37834  rngomndo  37895  pridl  37997  smprngopr  38012  ispridlc  38030  sn-isghm  42628  setindtrs  42982  dford3lem2  42984  dfac11  43019  rp-intrabeq  43182  rp-unirabeq  43183  rp-brsslt  43385  mnuop123d  44231  fnchoice  44929  axccdom  45129  axccd  45136  stoweidlem31  45952  stoweidlem57  45978  fourierdlem80  46107  fourierdlem103  46130  fourierdlem104  46131  isvonmbl  46559  paireqne  47385  requad2  47497  isthinc  48688  0thincg  48717  bnd2d  48773