Theorem raleq 3312

Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2130, ax-11 2147, and ax-12 2167. (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 3311	. . 3 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∃𝑥 ∈ 𝐵 ¬ 𝜑))
2		rexnal 3090	. . 3 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)
3		rexnal 3090	. . 3 ⊢ (∃𝑥 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐵 𝜑)
4	1, 2, 3	3bitr3g 312	. 2 ⊢ (𝐴 = 𝐵 → (¬ ∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐵 𝜑))
5	4	con4bid 316	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-ral 3052  df-rex 3061

This theorem is referenced by:  raleqi  3313  raleqdv  3315  sbralieALT  3343  r19.2zb  4490  inteq  4949  iineq1  5010  friOLD  5635  frsn  5761  fncnv  6624  isoeq4  7324  onminex  7803  tfisg  7856  tfinds  7862  f1oweALT  7978  frxp  8132  frxp2  8150  poseq  8164  frrlem1  8293  frrlem13  8305  wfrlem1OLD  8330  wfrlem15OLD  8345  tfrlem1  8398  tfrlem12  8411  omeulem1  8604  ixpeq1  8929  undifixp  8955  ac6sfi  9314  frfi  9315  iunfi  9378  indexfi  9397  supeq1  9481  supeq2  9484  brttrcl2  9750  ssttrcl  9751  ttrcltr  9752  bnd2  9929  acneq  10079  aceq3lem  10156  dfac5lem4  10162  dfac8  10171  dfac9  10172  kmlem1  10186  kmlem10  10195  kmlem13  10198  cfval  10281  axcc2lem  10470  axcc4dom  10475  axdc3lem3  10486  axdc3lem4  10487  ac4c  10510  ac5  10511  ac6sg  10522  zorn2lem7  10536  xrsupsslem  13334  xrinfmsslem  13335  xrsupss  13336  xrinfmss  13337  fsuppmapnn0fiubex  14006  rexanuz  15345  rexfiuz  15347  modfsummod  15793  gcdcllem3  16496  lcmfval  16617  lcmf0val  16618  lcmfunsnlem  16637  coprmprod  16657  coprmproddvds  16659  isprs  18317  drsdirfi  18325  isdrs2  18326  ispos  18334  pospropd  18347  lubeldm  18373  lubval  18376  glbeldm  18386  glbval  18389  istos  18438  isdlat  18542  mgmhmpropd  18686  mhmpropd  18777  isghm  19205  isghmOLD  19206  cntzval  19311  efgval  19711  iscmn  19783  rnghmval  20418  dfrhm2  20452  zrrnghm  20514  lidldvgen  21319  ocvval  21659  isobs  21714  coe1fzgsumd  22292  evl1gsumd  22345  mat0dimcrng  22460  mdetunilem9  22610  ist0  23312  cmpcovf  23383  is1stc  23433  2ndc1stc  23443  isref  23501  txflf  23998  ustuqtop4  24237  iscfilu  24281  ispsmet  24298  ismet  24317  isxmet  24318  cncfval  24896  lebnumlem3  24977  fmcfil  25288  iscfil3  25289  caucfil  25299  iscmet3  25309  cfilres  25312  minveclem3  25445  ovolfiniun  25518  finiunmbl  25561  volfiniun  25564  dvcn  25939  ulmval  26406  sltval2  27683  sltres  27689  nolesgn2o  27698  nogesgn1o  27700  nodense  27719  nosupbnd2lem1  27742  noinfbnd2lem1  27757  brsslt  27812  madebday  27920  negsprop  28041  mulsprop  28128  axtgcont1  28392  nb3grpr  29315  dfconngr1  30118  isconngr  30119  1conngr  30124  frgr0v  30192  isplig  30406  isgrpo  30427  isablo  30476  ocval  31210  acunirnmpt  32576  isomnd  32940  isorng  33182  prmidl  33321  ismbfm  34097  bnj865  34781  bnj1154  34857  bnj1296  34879  bnj1463  34913  wevgblacfn  34949  derangval  35008  setinds  35615  dfon2lem3  35622  dfon2lem7  35626  dfrecs2  35787  dfrdg4  35788  isfne  36064  finixpnum  37319  mblfinlem1  37371  mbfresfi  37380  indexdom  37448  heibor1lem  37523  isexid2  37569  ismndo2  37588  rngomndo  37649  pridl  37751  smprngopr  37766  ispridlc  37784  sn-isghm  42365  setindtrs  42720  dford3lem2  42722  dfac11  42760  rp-intrabeq  42923  rp-unirabeq  42924  rp-brsslt  43127  mnuop123d  43973  fnchoice  44665  axccdom  44865  axccd  44872  stoweidlem31  45688  stoweidlem57  45714  fourierdlem80  45843  fourierdlem103  45866  fourierdlem104  45867  isvonmbl  46295  paireqne  47119  requad2  47231  isthinc  48378  0thincg  48407  bnd2d  48463