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  18237  drsdirfi  18246  isdrs2  18247  ispos  18255  pospropd  18266  lubeldm  18292  lubval  18295  glbeldm  18305  glbval  18308  istos  18357  isdlat  18463  mgmhmpropd  18607  mhmpropd  18701  isghm  19129  isghmOLD  19130  cntzval  19235  efgval  19631  iscmn  19703  isomnd  20037  rnghmval  20360  dfrhm2  20394  zrrnghm  20456  isorng  20781  lidldvgen  21276  ocvval  21609  isobs  21662  coe1fzgsumd  22224  evl1gsumd  22277  mat0dimcrng  22390  mdetunilem9  22540  ist0  23240  cmpcovf  23311  is1stc  23361  2ndc1stc  23371  isref  23429  txflf  23926  ustuqtop4  24165  iscfilu  24208  ispsmet  24225  ismet  24244  isxmet  24245  cncfval  24814  lebnumlem3  24895  fmcfil  25205  iscfil3  25206  caucfil  25216  iscmet3  25226  cfilres  25229  minveclem3  25362  ovolfiniun  25435  finiunmbl  25478  volfiniun  25481  dvcn  25856  ulmval  26322  sltval2  27601  sltres  27607  nolesgn2o  27616  nogesgn1o  27618  nodense  27637  nosupbnd2lem1  27660  noinfbnd2lem1  27675  brsslt  27731  madebday  27849  negsprop  27981  mulsprop  28073  onsfi  28287  axtgcont1  28448  nb3grpr  29362  dfconngr1  30167  isconngr  30168  1conngr  30173  frgr0v  30241  isplig  30455  isgrpo  30476  isablo  30525  ocval  31259  acunirnmpt  32633  prmidl  33404  ismbfm  34234  bnj865  34906  bnj1154  34982  bnj1296  35004  bnj1463  35038  wevgblacfn  35089  derangval  35147  setinds  35759  dfon2lem3  35766  dfon2lem7  35770  dfrecs2  35931  dfrdg4  35932  isfne  36320  finixpnum  37592  mblfinlem1  37644  mbfresfi  37653  indexdom  37721  heibor1lem  37796  isexid2  37842  ismndo2  37861  rngomndo  37922  pridl  38024  smprngopr  38039  ispridlc  38057  sn-isghm  42654  setindtrs  43007  dford3lem2  43009  dfac11  43044  rp-intrabeq  43203  rp-unirabeq  43204  rp-brsslt  43405  mnuop123d  44244  relpeq4  44930  trfr  44945  permac8prim  44997  fnchoice  45016  axccdom  45209  axccd  45216  stoweidlem31  46022  stoweidlem57  46048  fourierdlem80  46177  fourierdlem103  46200  fourierdlem104  46201  isvonmbl  46629  paireqne  47505  requad2  47617  nelsubc3lem  49052  isthinc  49401  0thincg  49440  cnelsubclem  49585  bnd2d  49663