Theorem raleq 3293

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 3292	. . 3 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∃𝑥 ∈ 𝐵 ¬ 𝜑))
2		rexnal 3082	. . 3 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)
3		rexnal 3082	. . 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  3294  raleqdv  3296  raleleq  3312  sbralieALT  3324  r19.2zb  4455  inteq  4909  iineq1  4969  frsn  5719  fncnv  6573  isoeq4  7277  onminex  7758  tfisg  7810  tfinds  7816  f1oweALT  7930  frxp  8082  frxp2  8100  poseq  8114  frrlem1  8242  frrlem13  8254  tfrlem1  8321  tfrlem12  8334  omeulem1  8523  ixpeq1  8858  undifixp  8884  ac6sfi  9207  frfi  9208  iunfi  9270  indexfi  9287  supeq1  9372  supeq2  9375  brttrcl2  9643  ssttrcl  9644  ttrcltr  9645  bnd2  9822  acneq  9972  aceq3lem  10049  dfac5lem4  10055  dfac5lem4OLD  10057  dfac8  10065  dfac9  10066  kmlem1  10080  kmlem10  10089  kmlem13  10092  cfval  10176  axcc2lem  10365  axcc4dom  10370  axdc3lem3  10381  axdc3lem4  10382  ac4c  10405  ac5  10406  ac6sg  10417  zorn2lem7  10431  xrsupsslem  13243  xrinfmsslem  13244  xrsupss  13245  xrinfmss  13246  fsuppmapnn0fiubex  13933  rexanuz  15288  rexfiuz  15290  modfsummod  15736  gcdcllem3  16447  lcmfval  16567  lcmf0val  16568  lcmfunsnlem  16587  coprmprod  16607  coprmproddvds  16609  isprs  18233  drsdirfi  18242  isdrs2  18243  ispos  18251  pospropd  18262  lubeldm  18288  lubval  18291  glbeldm  18301  glbval  18304  istos  18353  isdlat  18457  mgmhmpropd  18601  mhmpropd  18695  isghm  19123  isghmOLD  19124  cntzval  19229  efgval  19623  iscmn  19695  rnghmval  20325  dfrhm2  20359  zrrnghm  20421  lidldvgen  21220  ocvval  21552  isobs  21605  coe1fzgsumd  22167  evl1gsumd  22220  mat0dimcrng  22333  mdetunilem9  22483  ist0  23183  cmpcovf  23254  is1stc  23304  2ndc1stc  23314  isref  23372  txflf  23869  ustuqtop4  24108  iscfilu  24151  ispsmet  24168  ismet  24187  isxmet  24188  cncfval  24757  lebnumlem3  24838  fmcfil  25148  iscfil3  25149  caucfil  25159  iscmet3  25169  cfilres  25172  minveclem3  25305  ovolfiniun  25378  finiunmbl  25421  volfiniun  25424  dvcn  25799  ulmval  26265  sltval2  27544  sltres  27550  nolesgn2o  27559  nogesgn1o  27561  nodense  27580  nosupbnd2lem1  27603  noinfbnd2lem1  27618  brsslt  27673  madebday  27787  negsprop  27917  mulsprop  28009  onsfi  28223  axtgcont1  28371  nb3grpr  29285  dfconngr1  30090  isconngr  30091  1conngr  30096  frgr0v  30164  isplig  30378  isgrpo  30399  isablo  30448  ocval  31182  acunirnmpt  32556  isomnd  32988  isorng  33250  prmidl  33384  ismbfm  34214  bnj865  34886  bnj1154  34962  bnj1296  34984  bnj1463  35018  wevgblacfn  35069  derangval  35127  setinds  35739  dfon2lem3  35746  dfon2lem7  35750  dfrecs2  35911  dfrdg4  35912  isfne  36300  finixpnum  37572  mblfinlem1  37624  mbfresfi  37633  indexdom  37701  heibor1lem  37776  isexid2  37822  ismndo2  37841  rngomndo  37902  pridl  38004  smprngopr  38019  ispridlc  38037  sn-isghm  42634  setindtrs  42987  dford3lem2  42989  dfac11  43024  rp-intrabeq  43183  rp-unirabeq  43184  rp-brsslt  43385  mnuop123d  44224  relpeq4  44910  trfr  44925  permac8prim  44977  fnchoice  44996  axccdom  45189  axccd  45196  stoweidlem31  46002  stoweidlem57  46028  fourierdlem80  46157  fourierdlem103  46180  fourierdlem104  46181  isvonmbl  46609  paireqne  47485  requad2  47597  nelsubc3lem  49032  isthinc  49381  0thincg  49420  cnelsubclem  49565  bnd2d  49643