Theorem raleq 3291

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   = wceq 1541  ∀wral 3049  ∃wrex 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-ral 3050  df-rex 3059

This theorem is referenced by:  raleqi  3292  raleqdv  3294  raleleq  3310  sbralieALT  3321  inteq  4903  iineq1  4962  frsn  5710  fncnv  6563  isoeq4  7264  onminex  7745  tfisg  7794  tfinds  7800  f1oweALT  7914  frxp  8066  frxp2  8084  poseq  8098  frrlem1  8226  frrlem13  8238  tfrlem1  8305  tfrlem12  8318  omeulem1  8507  ixpeq1  8844  undifixp  8870  ac6sfi  9182  frfi  9183  iunfi  9241  indexfi  9258  supeq1  9346  supeq2  9349  brttrcl2  9621  ssttrcl  9622  ttrcltr  9623  setinds  9656  bnd2  9803  acneq  9951  aceq3lem  10028  dfac5lem4  10034  dfac5lem4OLD  10036  dfac8  10044  dfac9  10045  kmlem1  10059  kmlem10  10068  kmlem13  10071  cfval  10155  axcc2lem  10344  axcc4dom  10349  axdc3lem3  10360  axdc3lem4  10361  ac4c  10384  ac5  10385  ac6sg  10396  zorn2lem7  10410  xrsupsslem  13220  xrinfmsslem  13221  xrsupss  13222  xrinfmss  13223  fsuppmapnn0fiubex  13913  rexanuz  15267  rexfiuz  15269  modfsummod  15715  gcdcllem3  16426  lcmfval  16546  lcmf0val  16547  lcmfunsnlem  16566  coprmprod  16586  coprmproddvds  16588  isprs  18217  drsdirfi  18226  isdrs2  18227  ispos  18235  pospropd  18246  lubeldm  18272  lubval  18275  glbeldm  18285  glbval  18288  istos  18337  isdlat  18443  mgmhmpropd  18621  mhmpropd  18715  isghm  19142  isghmOLD  19143  cntzval  19248  efgval  19644  iscmn  19716  isomnd  20050  rnghmval  20374  dfrhm2  20408  zrrnghm  20467  isorng  20792  lidldvgen  21287  ocvval  21620  isobs  21673  coe1fzgsumd  22246  evl1gsumd  22299  mat0dimcrng  22412  mdetunilem9  22562  ist0  23262  cmpcovf  23333  is1stc  23383  2ndc1stc  23393  isref  23451  txflf  23948  ustuqtop4  24186  iscfilu  24229  ispsmet  24246  ismet  24265  isxmet  24266  cncfval  24835  lebnumlem3  24916  fmcfil  25226  iscfil3  25227  caucfil  25237  iscmet3  25247  cfilres  25250  minveclem3  25383  ovolfiniun  25456  finiunmbl  25499  volfiniun  25502  dvcn  25877  ulmval  26343  sltval2  27622  sltres  27628  nolesgn2o  27637  nogesgn1o  27639  nodense  27658  nosupbnd2lem1  27681  noinfbnd2lem1  27696  brsslt  27752  madebday  27872  negsprop  28004  mulsprop  28099  onsfi  28316  axtgcont1  28489  nb3grpr  29404  dfconngr1  30212  isconngr  30213  1conngr  30218  frgr0v  30286  isplig  30500  isgrpo  30521  isablo  30570  ocval  31304  acunirnmpt  32686  prmidl  33470  ismbfm  34357  bnj865  35028  bnj1154  35104  bnj1296  35126  bnj1463  35160  r1filimi  35208  wevgblacfn  35252  derangval  35310  dfon2lem3  35926  dfon2lem7  35930  dfrecs2  36093  dfrdg4  36094  isfne  36482  finixpnum  37745  mblfinlem1  37797  mbfresfi  37806  indexdom  37874  heibor1lem  37949  isexid2  37995  ismndo2  38014  rngomndo  38075  pridl  38177  smprngopr  38192  ispridlc  38210  sn-isghm  42858  setindtrs  43209  dford3lem2  43211  dfac11  43246  rp-intrabeq  43405  rp-unirabeq  43406  rp-brsslt  43606  mnuop123d  44445  relpeq4  45130  trfr  45145  permac8prim  45197  fnchoice  45216  axccdom  45408  axccd  45415  stoweidlem31  46217  stoweidlem57  46243  fourierdlem80  46372  fourierdlem103  46395  fourierdlem104  46396  isvonmbl  46824  paireqne  47699  requad2  47811  nelsubc3lem  49257  isthinc  49606  0thincg  49645  cnelsubclem  49790  bnd2d  49868