Theorem raleq 3317

Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2175, ax-11 2191, and ax-12 2212. (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 3316	. . 3 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∃𝑥 ∈ 𝐵 ¬ 𝜑))
2		rexnal 3114	. . 3 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)
3		rexnal 3114	. . 3 ⊢ (∃𝑥 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐵 𝜑)
4	1, 2, 3	3bitr3g 315	. 2 ⊢ (𝐴 = 𝐵 → (¬ ∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐵 𝜑))
5	4	con4bid 319	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   = wceq 1560  ∀wral 3076  ∃wrex 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-ral 3077  df-rex 3087

This theorem is referenced by:  raleqi  3318  raleqdv  3320  raleleq  3332  sbralieALT  3341  inteq  4908  iineq1  4967  frsn  5735  fncnv  6594  isoeq4  7304  onminex  7785  tfisg  7834  tfinds  7840  f1oweALT  7953  frxp  8106  frxp2  8124  poseq  8138  frrlem1  8267  frrlem13  8279  tfrlem1  8346  tfrlem12  8360  omeulem1  8551  ixpeq1  8890  undifixp  8916  ac6sfi  9228  frfi  9229  iunfi  9286  indexfi  9303  supeq1  9391  supeq2  9394  brttrcl2  9669  ssttrcl  9670  ttrcltr  9671  setinds  9704  bnd2  9851  acneq  9999  aceq3lem  10076  dfac5lem4  10082  dfac5lem4OLD  10084  dfac8  10092  dfac9  10093  kmlem1  10107  kmlem10  10116  kmlem13  10119  cfval  10203  axcc2lem  10393  axcc4dom  10398  axdc3lem3  10409  axdc3lem4  10410  ac4c  10433  ac5  10434  ac6sg  10445  zorn2lem7  10459  xrsupsslem  13310  xrinfmsslem  13311  xrsupss  13312  xrinfmss  13313  fsuppmapnn0fiubex  14005  rexanuz  15373  rexfiuz  15375  modfsummod  15822  gcdcllem3  16535  lcmfval  16655  lcmf0val  16656  lcmfunsnlem  16675  coprmprod  16695  coprmproddvds  16697  isprs  18328  drsdirfi  18337  isdrs2  18338  ispos  18346  pospropd  18357  lubeldm  18383  lubval  18386  glbeldm  18396  glbval  18399  istos  18448  isdlat  18554  mgmhmpropd  18732  mhmpropd  18826  isghm  19256  cntzval  19361  efgval  19757  iscmn  19829  isomnd  20163  rnghmval  20489  dfrhm2  20523  zrrnghm  20586  isorng  20910  lidldvgen  21404  ocvval  21719  isobs  21772  coe1fzgsumd  22367  evl1gsumd  22420  mat0dimcrng  22530  mdetunilem9  22680  ist0  23380  cmpcovf  23451  is1stc  23501  2ndc1stc  23511  isref  23569  txflf  24066  ustuqtop4  24304  iscfilu  24347  ispsmet  24364  ismet  24383  isxmet  24384  cncfval  24950  lebnumlem3  25025  fmcfil  25334  iscfil3  25335  caucfil  25345  iscmet3  25355  cfilres  25358  minveclem3  25491  ovolfiniun  25563  finiunmbl  25606  volfiniun  25609  dvcn  25983  ulmval  26443  ltsval2  27720  ltsres  27726  nolesgn2o  27735  nogesgn1o  27737  nodense  27756  nosupbnd2lem1  27779  noinfbnd2lem1  27794  brslts  27855  madebday  27993  negsprop  28128  mulsprop  28223  onsfi  28449  axtgcont1  28637  nb3grpr  29583  dfconngr1  30390  isconngr  30391  1conngr  30396  frgr0v  30464  isplig  30679  isgrpo  30700  isablo  30749  ocval  31483  acunirnmpt  32861  prmidl  33626  ismbfm  34548  bnj865  35218  bnj1154  35294  bnj1296  35316  bnj1463  35350  r1filimi  35399  wevgblacfn  35454  derangval  35517  dfon2lem3  36133  dfon2lem7  36137  dfrecs2  36300  dfrdg4  36301  isfne  36699  finixpnum  38104  mblfinlem1  38156  mbfresfi  38165  indexdom  38233  heibor1lem  38308  isexid2  38354  ismndo2  38373  rngomndo  38434  pridl  38536  smprngopr  38551  ispridlc  38569  sn-isghm  43255  setindtrs  43602  dford3lem2  43604  dfac11  43639  rp-intrabeq  43798  rp-unirabeq  43799  rp-brsslt  43999  mnuop123d  44838  relpeq4  45523  trfr  45538  permac8prim  45590  fnchoice  45609  axccdom  45798  axccd  45804  stoweidlem31  46605  stoweidlem57  46631  fourierdlem80  46760  fourierdlem103  46783  fourierdlem104  46784  isvonmbl  47212  paireqne  48117  requad2  48245  nelsubc3lem  49691  isthinc  50040  0thincg  50079  cnelsubclem  50224  bnd2d  50302