Theorem raleq 3323

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

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

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 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ral 3062  df-rex 3071

This theorem is referenced by:  raleqi  3324  raleqdv  3326  raleleq  3342  sbralieALT  3359  r19.2zb  4496  inteq  4949  iineq1  5009  friOLD  5643  frsn  5773  fncnv  6639  isoeq4  7340  onminex  7822  tfisg  7875  tfinds  7881  f1oweALT  7997  frxp  8151  frxp2  8169  poseq  8183  frrlem1  8311  frrlem13  8323  wfrlem1OLD  8348  wfrlem15OLD  8363  tfrlem1  8416  tfrlem12  8429  omeulem1  8620  ixpeq1  8948  undifixp  8974  ac6sfi  9320  frfi  9321  iunfi  9383  indexfi  9400  supeq1  9485  supeq2  9488  brttrcl2  9754  ssttrcl  9755  ttrcltr  9756  bnd2  9933  acneq  10083  aceq3lem  10160  dfac5lem4  10166  dfac5lem4OLD  10168  dfac8  10176  dfac9  10177  kmlem1  10191  kmlem10  10200  kmlem13  10203  cfval  10287  axcc2lem  10476  axcc4dom  10481  axdc3lem3  10492  axdc3lem4  10493  ac4c  10516  ac5  10517  ac6sg  10528  zorn2lem7  10542  xrsupsslem  13349  xrinfmsslem  13350  xrsupss  13351  xrinfmss  13352  fsuppmapnn0fiubex  14033  rexanuz  15384  rexfiuz  15386  modfsummod  15830  gcdcllem3  16538  lcmfval  16658  lcmf0val  16659  lcmfunsnlem  16678  coprmprod  16698  coprmproddvds  16700  isprs  18342  drsdirfi  18351  isdrs2  18352  ispos  18360  pospropd  18372  lubeldm  18398  lubval  18401  glbeldm  18411  glbval  18414  istos  18463  isdlat  18567  mgmhmpropd  18711  mhmpropd  18805  isghm  19233  isghmOLD  19234  cntzval  19339  efgval  19735  iscmn  19807  rnghmval  20440  dfrhm2  20474  zrrnghm  20536  lidldvgen  21344  ocvval  21685  isobs  21740  coe1fzgsumd  22308  evl1gsumd  22361  mat0dimcrng  22476  mdetunilem9  22626  ist0  23328  cmpcovf  23399  is1stc  23449  2ndc1stc  23459  isref  23517  txflf  24014  ustuqtop4  24253  iscfilu  24297  ispsmet  24314  ismet  24333  isxmet  24334  cncfval  24914  lebnumlem3  24995  fmcfil  25306  iscfil3  25307  caucfil  25317  iscmet3  25327  cfilres  25330  minveclem3  25463  ovolfiniun  25536  finiunmbl  25579  volfiniun  25582  dvcn  25957  ulmval  26423  sltval2  27701  sltres  27707  nolesgn2o  27716  nogesgn1o  27718  nodense  27737  nosupbnd2lem1  27760  noinfbnd2lem1  27775  brsslt  27830  madebday  27938  negsprop  28067  mulsprop  28156  axtgcont1  28476  nb3grpr  29399  dfconngr1  30207  isconngr  30208  1conngr  30213  frgr0v  30281  isplig  30495  isgrpo  30516  isablo  30565  ocval  31299  acunirnmpt  32669  isomnd  33078  isorng  33329  prmidl  33468  ismbfm  34252  bnj865  34937  bnj1154  35013  bnj1296  35035  bnj1463  35069  wevgblacfn  35114  derangval  35172  setinds  35779  dfon2lem3  35786  dfon2lem7  35790  dfrecs2  35951  dfrdg4  35952  isfne  36340  finixpnum  37612  mblfinlem1  37664  mbfresfi  37673  indexdom  37741  heibor1lem  37816  isexid2  37862  ismndo2  37881  rngomndo  37942  pridl  38044  smprngopr  38059  ispridlc  38077  sn-isghm  42683  setindtrs  43037  dford3lem2  43039  dfac11  43074  rp-intrabeq  43233  rp-unirabeq  43234  rp-brsslt  43436  mnuop123d  44281  relpeq4  44968  trfr  44979  fnchoice  45034  axccdom  45227  axccd  45234  stoweidlem31  46046  stoweidlem57  46072  fourierdlem80  46201  fourierdlem103  46224  fourierdlem104  46225  isvonmbl  46653  paireqne  47498  requad2  47610  isthinc  49069  0thincg  49107  bnd2d  49200