Theorem raleq 3292

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ral 3052  df-rex 3062

This theorem is referenced by:  raleqi  3293  raleqdv  3295  raleleq  3307  sbralieALT  3316  inteq  4892  iineq1  4951  frsn  5719  fncnv  6571  isoeq4  7275  onminex  7756  tfisg  7805  tfinds  7811  f1oweALT  7925  frxp  8076  frxp2  8094  poseq  8108  frrlem1  8236  frrlem13  8248  tfrlem1  8315  tfrlem12  8328  omeulem1  8517  ixpeq1  8856  undifixp  8882  ac6sfi  9194  frfi  9195  iunfi  9253  indexfi  9270  supeq1  9358  supeq2  9361  brttrcl2  9635  ssttrcl  9636  ttrcltr  9637  setinds  9670  bnd2  9817  acneq  9965  aceq3lem  10042  dfac5lem4  10048  dfac5lem4OLD  10050  dfac8  10058  dfac9  10059  kmlem1  10073  kmlem10  10082  kmlem13  10085  cfval  10169  axcc2lem  10358  axcc4dom  10363  axdc3lem3  10374  axdc3lem4  10375  ac4c  10398  ac5  10399  ac6sg  10410  zorn2lem7  10424  xrsupsslem  13259  xrinfmsslem  13260  xrsupss  13261  xrinfmss  13262  fsuppmapnn0fiubex  13954  rexanuz  15308  rexfiuz  15310  modfsummod  15757  gcdcllem3  16470  lcmfval  16590  lcmf0val  16591  lcmfunsnlem  16610  coprmprod  16630  coprmproddvds  16632  isprs  18262  drsdirfi  18271  isdrs2  18272  ispos  18280  pospropd  18291  lubeldm  18317  lubval  18320  glbeldm  18330  glbval  18333  istos  18382  isdlat  18488  mgmhmpropd  18666  mhmpropd  18760  isghm  19190  isghmOLD  19191  cntzval  19296  efgval  19692  iscmn  19764  isomnd  20098  rnghmval  20420  dfrhm2  20454  zrrnghm  20513  isorng  20838  lidldvgen  21332  ocvval  21647  isobs  21700  coe1fzgsumd  22269  evl1gsumd  22322  mat0dimcrng  22435  mdetunilem9  22585  ist0  23285  cmpcovf  23356  is1stc  23406  2ndc1stc  23416  isref  23474  txflf  23971  ustuqtop4  24209  iscfilu  24252  ispsmet  24269  ismet  24288  isxmet  24289  cncfval  24855  lebnumlem3  24930  fmcfil  25239  iscfil3  25240  caucfil  25250  iscmet3  25260  cfilres  25263  minveclem3  25396  ovolfiniun  25468  finiunmbl  25511  volfiniun  25514  dvcn  25888  ulmval  26345  ltsval2  27620  ltsres  27626  nolesgn2o  27635  nogesgn1o  27637  nodense  27656  nosupbnd2lem1  27679  noinfbnd2lem1  27694  brslts  27754  madebday  27892  negsprop  28027  mulsprop  28122  onsfi  28348  axtgcont1  28536  nb3grpr  29451  dfconngr1  30258  isconngr  30259  1conngr  30264  frgr0v  30332  isplig  30547  isgrpo  30568  isablo  30617  ocval  31351  acunirnmpt  32732  prmidl  33500  ismbfm  34395  bnj865  35065  bnj1154  35141  bnj1296  35163  bnj1463  35197  r1filimi  35246  wevgblacfn  35291  derangval  35349  dfon2lem3  35965  dfon2lem7  35969  dfrecs2  36132  dfrdg4  36133  isfne  36521  finixpnum  37926  mblfinlem1  37978  mbfresfi  37987  indexdom  38055  heibor1lem  38130  isexid2  38176  ismndo2  38195  rngomndo  38256  pridl  38358  smprngopr  38373  ispridlc  38391  sn-isghm  43106  setindtrs  43453  dford3lem2  43455  dfac11  43490  rp-intrabeq  43649  rp-unirabeq  43650  rp-brsslt  43850  mnuop123d  44689  relpeq4  45374  trfr  45389  permac8prim  45441  fnchoice  45460  axccdom  45651  axccd  45658  stoweidlem31  46459  stoweidlem57  46485  fourierdlem80  46614  fourierdlem103  46637  fourierdlem104  46638  isvonmbl  47066  paireqne  47971  requad2  48099  nelsubc3lem  49545  isthinc  49894  0thincg  49933  cnelsubclem  50078  bnd2d  50156