Theorem raleq 3294

Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2152, ax-11 2168, and ax-12 2189. (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 3293	. . 3 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∃𝑥 ∈ 𝐵 ¬ 𝜑))
2		rexnal 3091	. . 3 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)
3		rexnal 3091	. . 3 ⊢ (∃𝑥 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐵 𝜑)
4	1, 2, 3	3bitr3g 314	. 2 ⊢ (𝐴 = 𝐵 → (¬ ∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐵 𝜑))
5	4	con4bid 318	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   = wceq 1547  ∀wral 3053  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ral 3054  df-rex 3064

This theorem is referenced by:  raleqi  3295  raleqdv  3297  raleleq  3309  sbralieALT  3318  inteq  4880  iineq1  4939  frsn  5706  fncnv  6558  isoeq4  7264  onminex  7745  tfisg  7794  tfinds  7800  f1oweALT  7914  frxp  8066  frxp2  8084  poseq  8098  frrlem1  8226  frrlem13  8238  tfrlem1  8305  tfrlem12  8318  omeulem1  8507  ixpeq1  8846  undifixp  8872  ac6sfi  9184  frfi  9185  iunfi  9243  indexfi  9260  supeq1  9348  supeq2  9351  brttrcl2  9626  ssttrcl  9627  ttrcltr  9628  setinds  9661  bnd2  9808  acneq  9956  aceq3lem  10033  dfac5lem4  10039  dfac5lem4OLD  10041  dfac8  10049  dfac9  10050  kmlem1  10064  kmlem10  10073  kmlem13  10076  cfval  10160  axcc2lem  10349  axcc4dom  10354  axdc3lem3  10365  axdc3lem4  10366  ac4c  10389  ac5  10390  ac6sg  10401  zorn2lem7  10415  xrsupsslem  13250  xrinfmsslem  13251  xrsupss  13252  xrinfmss  13253  fsuppmapnn0fiubex  13945  rexanuz  15299  rexfiuz  15301  modfsummod  15748  gcdcllem3  16461  lcmfval  16581  lcmf0val  16582  lcmfunsnlem  16601  coprmprod  16621  coprmproddvds  16623  isprs  18253  drsdirfi  18262  isdrs2  18263  ispos  18271  pospropd  18282  lubeldm  18308  lubval  18311  glbeldm  18321  glbval  18324  istos  18373  isdlat  18479  mgmhmpropd  18657  mhmpropd  18751  isghm  19181  isghmOLD  19182  cntzval  19287  efgval  19683  iscmn  19755  isomnd  20089  rnghmval  20411  dfrhm2  20445  zrrnghm  20508  isorng  20833  lidldvgen  21327  ocvval  21642  isobs  21695  coe1fzgsumd  22290  evl1gsumd  22343  mat0dimcrng  22453  mdetunilem9  22603  ist0  23303  cmpcovf  23374  is1stc  23424  2ndc1stc  23434  isref  23492  txflf  23989  ustuqtop4  24227  iscfilu  24270  ispsmet  24287  ismet  24306  isxmet  24307  cncfval  24873  lebnumlem3  24948  fmcfil  25257  iscfil3  25258  caucfil  25268  iscmet3  25278  cfilres  25281  minveclem3  25414  ovolfiniun  25486  finiunmbl  25529  volfiniun  25532  dvcn  25906  ulmval  26363  ltsval2  27638  ltsres  27644  nolesgn2o  27653  nogesgn1o  27655  nodense  27674  nosupbnd2lem1  27697  noinfbnd2lem1  27712  brslts  27772  madebday  27910  negsprop  28045  mulsprop  28140  onsfi  28366  axtgcont1  28554  nb3grpr  29469  dfconngr1  30276  isconngr  30277  1conngr  30282  frgr0v  30350  isplig  30565  isgrpo  30586  isablo  30635  ocval  31369  acunirnmpt  32751  prmidl  33523  ismbfm  34435  bnj865  35105  bnj1154  35181  bnj1296  35203  bnj1463  35237  r1filimi  35284  wevgblacfn  35337  derangval  35395  dfon2lem3  36011  dfon2lem7  36015  dfrecs2  36178  dfrdg4  36179  isfne  36567  finixpnum  37972  mblfinlem1  38024  mbfresfi  38033  indexdom  38101  heibor1lem  38176  isexid2  38222  ismndo2  38241  rngomndo  38302  pridl  38404  smprngopr  38419  ispridlc  38437  sn-isghm  43123  setindtrs  43470  dford3lem2  43472  dfac11  43507  rp-intrabeq  43666  rp-unirabeq  43667  rp-brsslt  43867  mnuop123d  44706  relpeq4  45391  trfr  45406  permac8prim  45458  fnchoice  45477  axccdom  45667  axccd  45673  stoweidlem31  46474  stoweidlem57  46500  fourierdlem80  46629  fourierdlem103  46652  fourierdlem104  46653  isvonmbl  47081  paireqne  47986  requad2  48114  nelsubc3lem  49560  isthinc  49909  0thincg  49948  cnelsubclem  50093  bnd2d  50171