Theorem raleq 3326

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1567  ∀wral 3085  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ral 3086  df-rex 3096

This theorem is referenced by:  raleqi  3327  raleqdv  3329  raleleq  3341  sbralieALT  3350  inteq  4919  iineq1  4978  frsn  5750  fncnv  6610  isoeq4  7319  onminex  7800  tfisg  7849  tfinds  7855  f1oweALT  7968  frxp  8121  frxp2  8139  poseq  8153  frrlem1  8282  frrlem13  8294  tfrlem1  8361  tfrlem12  8375  omeulem1  8566  ixpeq1  8905  undifixp  8931  ac6sfi  9243  frfi  9244  iunfi  9299  indexfi  9316  supeq1  9404  supeq2  9407  brttrcl2  9682  ssttrcl  9683  ttrcltr  9684  setinds  9717  bnd2  9878  acneq  10026  aceq3lem  10103  dfac5lem4  10109  dfac8  10118  dfac9  10119  kmlem1  10133  kmlem10  10142  kmlem13  10145  cfval  10229  axcc2lem  10419  axcc4dom  10424  axdc3lem3  10435  axdc3lem4  10436  ac4c  10459  ac5  10460  ac6sg  10471  zorn2lem7  10485  xrsupsslem  13332  xrinfmsslem  13333  xrsupss  13334  xrinfmss  13335  fsuppmapnn0fiubex  14027  rexanuz  15396  rexfiuz  15398  modfsummod  15845  gcdcllem3  16558  lcmfval  16678  lcmf0val  16679  lcmfunsnlem  16698  coprmprod  16718  coprmproddvds  16720  isprs  18351  drsdirfi  18360  isdrs2  18361  ispos  18369  pospropd  18380  lubeldm  18406  lubval  18409  glbeldm  18419  glbval  18422  istos  18471  isdlat  18577  mgmhmpropd  18755  mhmpropd  18849  isghm  19285  cntzval  19390  efgval  19786  iscmn  19858  isomnd  20192  rnghmval  20521  dfrhm2  20555  zrrnghm  20620  isorng  20941  prmidl  21435  lidldvgen  21470  ocvval  21785  isobs  21838  coe1fzgsumd  22432  evl1gsumd  22485  mat0dimcrng  22595  mdetunilem9  22745  ist0  23445  cmpcovf  23516  is1stc  23566  2ndc1stc  23576  isref  23634  txflf  24131  ustuqtop4  24369  iscfilu  24412  ispsmet  24429  ismet  24448  isxmet  24449  cncfval  25015  lebnumlem3  25090  fmcfil  25399  iscfil3  25400  caucfil  25410  iscmet3  25420  cfilres  25423  minveclem3  25556  ovolfiniun  25628  finiunmbl  25671  volfiniun  25674  dvcn  26048  ulmval  26508  ltsval2  27785  ltsres  27791  nolesgn2o  27800  nogesgn1o  27802  nodense  27821  nosupbnd2lem1  27844  noinfbnd2lem1  27859  brslts  27920  madebday  28058  negsprop  28193  mulsprop  28288  onsfi  28514  axtgcont1  28702  nb3grpr  29672  dfconngr1  30479  isconngr  30480  1conngr  30485  frgr0v  30553  isplig  30768  isgrpo  30789  isablo  30838  ocval  31572  acunirnmpt  32944  ismbfm  34585  bnj865  35255  bnj1154  35331  bnj1296  35353  bnj1463  35387  r1filimi  35438  wevgblacfn  35493  derangval  35557  dfon2lem3  36173  dfon2lem7  36177  dfrecs2  36340  dfrdg4  36341  isfne  36738  finixpnum  38143  mblfinlem1  38195  mbfresfi  38204  indexdom  38272  heibor1lem  38347  isexid2  38393  ismndo2  38412  rngomndo  38473  pridl  38575  smprngopr  38590  ispridlc  38608  sn-isghm  43296  setindtrs  43643  dford3lem2  43645  dfac11  43680  rp-intrabeq  43839  rp-unirabeq  43840  rp-brsslt  44040  mnuop123d  44863  relpeq4  45547  trfr  45562  permac8prim  45614  fnchoice  45640  axccdom  45829  axccd  45835  stoweidlem31  46636  stoweidlem57  46662  fourierdlem80  46791  fourierdlem103  46814  fourierdlem104  46815  isvonmbl  47243  paireqne  48148  requad2  48276  smprngprmrng  48992  nelsubc3lem  49732  isthinc  50081  0thincg  50120  cnelsubclem  50265  bnd2d  50343