Theorem raleq 3296

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   = wceq 1540  ∀wral 3044  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ral 3045  df-rex 3054

This theorem is referenced by:  raleqi  3297  raleqdv  3299  raleleq  3315  sbralieALT  3327  r19.2zb  4459  inteq  4913  iineq1  4973  frsn  5726  fncnv  6589  isoeq4  7295  onminex  7778  tfisg  7830  tfinds  7836  f1oweALT  7951  frxp  8105  frxp2  8123  poseq  8137  frrlem1  8265  frrlem13  8277  tfrlem1  8344  tfrlem12  8357  omeulem1  8546  ixpeq1  8881  undifixp  8907  ac6sfi  9231  frfi  9232  iunfi  9294  indexfi  9311  supeq1  9396  supeq2  9399  brttrcl2  9667  ssttrcl  9668  ttrcltr  9669  bnd2  9846  acneq  9996  aceq3lem  10073  dfac5lem4  10079  dfac5lem4OLD  10081  dfac8  10089  dfac9  10090  kmlem1  10104  kmlem10  10113  kmlem13  10116  cfval  10200  axcc2lem  10389  axcc4dom  10394  axdc3lem3  10405  axdc3lem4  10406  ac4c  10429  ac5  10430  ac6sg  10441  zorn2lem7  10455  xrsupsslem  13267  xrinfmsslem  13268  xrsupss  13269  xrinfmss  13270  fsuppmapnn0fiubex  13957  rexanuz  15312  rexfiuz  15314  modfsummod  15760  gcdcllem3  16471  lcmfval  16591  lcmf0val  16592  lcmfunsnlem  16611  coprmprod  16631  coprmproddvds  16633  isprs  18257  drsdirfi  18266  isdrs2  18267  ispos  18275  pospropd  18286  lubeldm  18312  lubval  18315  glbeldm  18325  glbval  18328  istos  18377  isdlat  18481  mgmhmpropd  18625  mhmpropd  18719  isghm  19147  isghmOLD  19148  cntzval  19253  efgval  19647  iscmn  19719  rnghmval  20349  dfrhm2  20383  zrrnghm  20445  lidldvgen  21244  ocvval  21576  isobs  21629  coe1fzgsumd  22191  evl1gsumd  22244  mat0dimcrng  22357  mdetunilem9  22507  ist0  23207  cmpcovf  23278  is1stc  23328  2ndc1stc  23338  isref  23396  txflf  23893  ustuqtop4  24132  iscfilu  24175  ispsmet  24192  ismet  24211  isxmet  24212  cncfval  24781  lebnumlem3  24862  fmcfil  25172  iscfil3  25173  caucfil  25183  iscmet3  25193  cfilres  25196  minveclem3  25329  ovolfiniun  25402  finiunmbl  25445  volfiniun  25448  dvcn  25823  ulmval  26289  sltval2  27568  sltres  27574  nolesgn2o  27583  nogesgn1o  27585  nodense  27604  nosupbnd2lem1  27627  noinfbnd2lem1  27642  brsslt  27697  madebday  27811  negsprop  27941  mulsprop  28033  onsfi  28247  axtgcont1  28395  nb3grpr  29309  dfconngr1  30117  isconngr  30118  1conngr  30123  frgr0v  30191  isplig  30405  isgrpo  30426  isablo  30475  ocval  31209  acunirnmpt  32583  isomnd  33015  isorng  33277  prmidl  33411  ismbfm  34241  bnj865  34913  bnj1154  34989  bnj1296  35011  bnj1463  35045  wevgblacfn  35096  derangval  35154  setinds  35766  dfon2lem3  35773  dfon2lem7  35777  dfrecs2  35938  dfrdg4  35939  isfne  36327  finixpnum  37599  mblfinlem1  37651  mbfresfi  37660  indexdom  37728  heibor1lem  37803  isexid2  37849  ismndo2  37868  rngomndo  37929  pridl  38031  smprngopr  38046  ispridlc  38064  sn-isghm  42661  setindtrs  43014  dford3lem2  43016  dfac11  43051  rp-intrabeq  43210  rp-unirabeq  43211  rp-brsslt  43412  mnuop123d  44251  relpeq4  44937  trfr  44952  permac8prim  45004  fnchoice  45023  axccdom  45216  axccd  45223  stoweidlem31  46029  stoweidlem57  46055  fourierdlem80  46184  fourierdlem103  46207  fourierdlem104  46208  isvonmbl  46636  paireqne  47512  requad2  47624  nelsubc3lem  49059  isthinc  49408  0thincg  49447  cnelsubclem  49592  bnd2d  49670