Theorem raleq 3316

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1569  ∀wral 3076  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ral 3077  df-rex 3087

This theorem is used by:  raleqi  3317  raleqdv  3319  raleleq  3331  sbralieALT  3339  inteq  4909  iineq1  4968  frsn  5740  fncnv  6618  isoeq4  7332  onminex  7820  tfisg  7869  tfinds  7875  f1oweALT  7988  frxp  8145  frxp2  8168  poseq  8182  frrlem1  8312  frrlem13  8324  tfrlem1  8391  tfrlem12  8405  omeulem1  8598  ixpeq1  8944  undifixp  8970  ac6sfi  9283  frfi  9284  iunfi  9340  indexfi  9357  supeq1  9444  supeq2  9447  brttrcl2  9722  ssttrcl  9723  ttrcltr  9724  setinds  9757  r1filimi  9910  bnd2  9963  bnd2d  9975  acneq  10129  aceq3lem  10206  dfac5lem4  10212  dfac8  10221  dfac9  10222  kmlem1  10236  kmlem10  10245  kmlem13  10248  cfval  10331  axcc2lem  10521  axcc4dom  10526  axdc3lem3  10537  axdc3lem4  10538  ac4c  10561  ac5  10562  ac6sg  10573  zorn2lem7  10587  xrsupsslem  13444  xrinfmsslem  13445  xrsupss  13446  xrinfmss  13447  fsuppmapnn0fiubex  14142  rexanuz  15522  rexfiuz  15524  modfsummod  15970  gcdcllem3  16680  lcmfval  16805  lcmf0val  16806  lcmfunsnlem  16825  coprmprod  16845  coprmproddvds  16847  isprs  18479  drsdirfi  18488  isdrs2  18489  ispos  18497  pospropd  18508  lubeldm  18534  lubval  18537  glbeldm  18547  glbval  18550  istos  18599  isdlat  18705  idressidex  18870  mgmhmpropd  18896  mhmpropd  18996  isghm  19439  cntzval  19544  efgval  19940  iscmn  20012  isomnd  20346  rnghmval  20679  dfrhm2  20713  rhmval0  20714  zrrnghm  20797  isorng  21127  prmidl  21630  lidldvgen  21667  ocvval  21982  isobs  22035  coe1fzgsumd  22631  evl1gsumd  22684  mat0dimcrng  22794  mdetunilem9  22944  ist0  23647  cmpcovf  23718  is1stc  23768  2ndc1stc  23778  isref  23837  txflf  24334  ustuqtop4  24572  iscfilu  24615  ispsmet  24632  ismet  24651  isxmet  24652  cncfval  25218  lebnumlem3  25293  fmcfil  25602  iscfil3  25603  caucfil  25613  iscmet3  25623  cfilres  25626  minveclem3  25759  ovolfiniun  25831  finiunmbl  25874  volfiniun  25877  dvcn  26250  ulmval  26716  ltsval2  28022  ltsres  28028  nolesgn2o  28037  nogesgn1o  28039  nodense  28058  nosupbnd2lem1  28081  noinfbnd2lem1  28096  brslts  28157  madebday  28295  negsprop  28430  mulsprop  28525  onsfi  28751  axtgcont1  28939  nb3grpr  29972  dfconngr1  30798  isconngr  30799  1conngr  30804  frgr0v  30872  isplig  31087  isgrpo  31108  isablo  31157  ocval  31891  acunirnmpt  33304  ismbfm  34934  bnj865  35603  bnj1154  35679  bnj1296  35701  bnj1463  35735  wevgblacfn  35990  derangval  36050  dfon2lem3  36671  dfon2lem7  36675  dfrecs2  36838  dfrdg4  36839  isfne  37251  finixpnum  38665  mblfinlem1  38712  mbfresfi  38721  indexdom  38805  heibor1lem  38880  isexid2  38926  ismndo2  38945  rngomndo  39006  pridl  39108  smprngopr  39123  ispridlc  39141  sn-isghm  43821  setindtrs  44169  dford3lem2  44171  dfac11  44201  rp-intrabeq  44360  rp-unirabeq  44361  rp-brsslt  44561  mnuop123d  45383  relpeq4  46073  trfr  46088  permac8prim  46140  fnchoice  46182  axccdom  46371  axccd  46377  stoweidlem31  47177  stoweidlem57  47203  fourierdlem80  47332  fourierdlem103  47355  fourierdlem104  47356  isvonmbl  47784  paireqne  48729  requad2  48857  smprngprmrng  49572  nelsubc3lem  50320  isthinc  50690  0thincg  50729  cnelsubcw  50877