Theorem raleq 3298

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 3297	. . 3 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∃𝑥 ∈ 𝐵 ¬ 𝜑))
2		rexnal 3083	. . 3 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)
3		rexnal 3083	. . 3 ⊢ (∃𝑥 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐵 𝜑)
4	1, 2, 3	3bitr3g 313	. 2 ⊢ (𝐴 = 𝐵 → (¬ ∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐵 𝜑))
5	4	con4bid 317	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ral 3046  df-rex 3055

This theorem is referenced by:  raleqi  3299  raleqdv  3301  raleleq  3317  sbralieALT  3329  r19.2zb  4462  inteq  4916  iineq1  4976  frsn  5729  fncnv  6592  isoeq4  7298  onminex  7781  tfisg  7833  tfinds  7839  f1oweALT  7954  frxp  8108  frxp2  8126  poseq  8140  frrlem1  8268  frrlem13  8280  tfrlem1  8347  tfrlem12  8360  omeulem1  8549  ixpeq1  8884  undifixp  8910  ac6sfi  9238  frfi  9239  iunfi  9301  indexfi  9318  supeq1  9403  supeq2  9406  brttrcl2  9674  ssttrcl  9675  ttrcltr  9676  bnd2  9853  acneq  10003  aceq3lem  10080  dfac5lem4  10086  dfac5lem4OLD  10088  dfac8  10096  dfac9  10097  kmlem1  10111  kmlem10  10120  kmlem13  10123  cfval  10207  axcc2lem  10396  axcc4dom  10401  axdc3lem3  10412  axdc3lem4  10413  ac4c  10436  ac5  10437  ac6sg  10448  zorn2lem7  10462  xrsupsslem  13274  xrinfmsslem  13275  xrsupss  13276  xrinfmss  13277  fsuppmapnn0fiubex  13964  rexanuz  15319  rexfiuz  15321  modfsummod  15767  gcdcllem3  16478  lcmfval  16598  lcmf0val  16599  lcmfunsnlem  16618  coprmprod  16638  coprmproddvds  16640  isprs  18264  drsdirfi  18273  isdrs2  18274  ispos  18282  pospropd  18293  lubeldm  18319  lubval  18322  glbeldm  18332  glbval  18335  istos  18384  isdlat  18488  mgmhmpropd  18632  mhmpropd  18726  isghm  19154  isghmOLD  19155  cntzval  19260  efgval  19654  iscmn  19726  rnghmval  20356  dfrhm2  20390  zrrnghm  20452  lidldvgen  21251  ocvval  21583  isobs  21636  coe1fzgsumd  22198  evl1gsumd  22251  mat0dimcrng  22364  mdetunilem9  22514  ist0  23214  cmpcovf  23285  is1stc  23335  2ndc1stc  23345  isref  23403  txflf  23900  ustuqtop4  24139  iscfilu  24182  ispsmet  24199  ismet  24218  isxmet  24219  cncfval  24788  lebnumlem3  24869  fmcfil  25179  iscfil3  25180  caucfil  25190  iscmet3  25200  cfilres  25203  minveclem3  25336  ovolfiniun  25409  finiunmbl  25452  volfiniun  25455  dvcn  25830  ulmval  26296  sltval2  27575  sltres  27581  nolesgn2o  27590  nogesgn1o  27592  nodense  27611  nosupbnd2lem1  27634  noinfbnd2lem1  27649  brsslt  27704  madebday  27818  negsprop  27948  mulsprop  28040  onsfi  28254  axtgcont1  28402  nb3grpr  29316  dfconngr1  30124  isconngr  30125  1conngr  30130  frgr0v  30198  isplig  30412  isgrpo  30433  isablo  30482  ocval  31216  acunirnmpt  32590  isomnd  33022  isorng  33284  prmidl  33418  ismbfm  34248  bnj865  34920  bnj1154  34996  bnj1296  35018  bnj1463  35052  wevgblacfn  35103  derangval  35161  setinds  35773  dfon2lem3  35780  dfon2lem7  35784  dfrecs2  35945  dfrdg4  35946  isfne  36334  finixpnum  37606  mblfinlem1  37658  mbfresfi  37667  indexdom  37735  heibor1lem  37810  isexid2  37856  ismndo2  37875  rngomndo  37936  pridl  38038  smprngopr  38053  ispridlc  38071  sn-isghm  42668  setindtrs  43021  dford3lem2  43023  dfac11  43058  rp-intrabeq  43217  rp-unirabeq  43218  rp-brsslt  43419  mnuop123d  44258  relpeq4  44944  trfr  44959  permac8prim  45011  fnchoice  45030  axccdom  45223  axccd  45230  stoweidlem31  46036  stoweidlem57  46062  fourierdlem80  46191  fourierdlem103  46214  fourierdlem104  46215  isvonmbl  46643  paireqne  47516  requad2  47628  nelsubc3lem  49063  isthinc  49412  0thincg  49451  cnelsubclem  49596  bnd2d  49674