Theorem raleq 3286

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 3285	. . 3 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∃𝑥 ∈ 𝐵 ¬ 𝜑))
2		rexnal 3081	. . 3 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)
3		rexnal 3081	. . 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  3287  raleqdv  3289  raleleq  3305  sbralieALT  3316  r19.2zb  4447  inteq  4899  iineq1  4959  frsn  5707  fncnv  6555  isoeq4  7257  onminex  7738  tfisg  7787  tfinds  7793  f1oweALT  7907  frxp  8059  frxp2  8077  poseq  8091  frrlem1  8219  frrlem13  8231  tfrlem1  8298  tfrlem12  8311  omeulem1  8500  ixpeq1  8835  undifixp  8861  ac6sfi  9173  frfi  9174  iunfi  9233  indexfi  9250  supeq1  9335  supeq2  9338  brttrcl2  9610  ssttrcl  9611  ttrcltr  9612  bnd2  9789  acneq  9937  aceq3lem  10014  dfac5lem4  10020  dfac5lem4OLD  10022  dfac8  10030  dfac9  10031  kmlem1  10045  kmlem10  10054  kmlem13  10057  cfval  10141  axcc2lem  10330  axcc4dom  10335  axdc3lem3  10346  axdc3lem4  10347  ac4c  10370  ac5  10371  ac6sg  10382  zorn2lem7  10396  xrsupsslem  13209  xrinfmsslem  13210  xrsupss  13211  xrinfmss  13212  fsuppmapnn0fiubex  13899  rexanuz  15253  rexfiuz  15255  modfsummod  15701  gcdcllem3  16412  lcmfval  16532  lcmf0val  16533  lcmfunsnlem  16552  coprmprod  16572  coprmproddvds  16574  isprs  18202  drsdirfi  18211  isdrs2  18212  ispos  18220  pospropd  18231  lubeldm  18257  lubval  18260  glbeldm  18270  glbval  18273  istos  18322  isdlat  18428  mgmhmpropd  18572  mhmpropd  18666  isghm  19094  isghmOLD  19095  cntzval  19200  efgval  19596  iscmn  19668  isomnd  20002  rnghmval  20325  dfrhm2  20359  zrrnghm  20421  isorng  20746  lidldvgen  21241  ocvval  21574  isobs  21627  coe1fzgsumd  22189  evl1gsumd  22242  mat0dimcrng  22355  mdetunilem9  22505  ist0  23205  cmpcovf  23276  is1stc  23326  2ndc1stc  23336  isref  23394  txflf  23891  ustuqtop4  24130  iscfilu  24173  ispsmet  24190  ismet  24209  isxmet  24210  cncfval  24779  lebnumlem3  24860  fmcfil  25170  iscfil3  25171  caucfil  25181  iscmet3  25191  cfilres  25194  minveclem3  25327  ovolfiniun  25400  finiunmbl  25443  volfiniun  25446  dvcn  25821  ulmval  26287  sltval2  27566  sltres  27572  nolesgn2o  27581  nogesgn1o  27583  nodense  27602  nosupbnd2lem1  27625  noinfbnd2lem1  27640  brsslt  27696  madebday  27814  negsprop  27946  mulsprop  28038  onsfi  28252  axtgcont1  28413  nb3grpr  29327  dfconngr1  30132  isconngr  30133  1conngr  30138  frgr0v  30206  isplig  30420  isgrpo  30441  isablo  30490  ocval  31224  acunirnmpt  32603  prmidl  33378  ismbfm  34224  bnj865  34896  bnj1154  34972  bnj1296  34994  bnj1463  35028  wevgblacfn  35092  derangval  35150  setinds  35762  dfon2lem3  35769  dfon2lem7  35773  dfrecs2  35934  dfrdg4  35935  isfne  36323  finixpnum  37595  mblfinlem1  37647  mbfresfi  37656  indexdom  37724  heibor1lem  37799  isexid2  37845  ismndo2  37864  rngomndo  37925  pridl  38027  smprngopr  38042  ispridlc  38060  sn-isghm  42656  setindtrs  43008  dford3lem2  43010  dfac11  43045  rp-intrabeq  43204  rp-unirabeq  43205  rp-brsslt  43406  mnuop123d  44245  relpeq4  44931  trfr  44946  permac8prim  44998  fnchoice  45017  axccdom  45210  axccd  45217  stoweidlem31  46022  stoweidlem57  46048  fourierdlem80  46177  fourierdlem103  46200  fourierdlem104  46201  isvonmbl  46629  paireqne  47505  requad2  47617  nelsubc3lem  49065  isthinc  49414  0thincg  49453  cnelsubclem  49598  bnd2d  49676