MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexeq Structured version   Visualization version   GIF version

Theorem rexeq 3286
Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.)
Assertion
Ref Expression
rexeq (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rexeq
StepHypRef Expression
1 nfcv 2906 . 2 𝑥𝐴
2 nfcv 2906 . 2 𝑥𝐵
31, 2rexeqf 3282 1 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1652  wrex 3055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2742
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-cleq 2757  df-clel 2760  df-nfc 2895  df-rex 3060
This theorem is referenced by:  rexeqi  3290  rexeqdv  3292  rexeqbi1dv  3294  unieq  4601  exss  5086  qseq1  7998  1sdom  8369  pssnn  8384  indexfi  8480  supeq1  8557  bnd2  8970  dfac2b  9203  dfac2OLD  9205  cflem  9320  cflecard  9327  cfeq0  9330  cfsuc  9331  cfflb  9333  cofsmo  9343  elwina  9760  eltskg  9824  rankcf  9851  elnp  10061  elnpi  10062  genpv  10073  xrsupsslem  12338  xrinfmsslem  12339  xrsupss  12340  xrinfmss  12341  hashge2el2difr  13463  isdrs  17201  isipodrs  17428  neifval  21182  ishaus  21405  2ndc1stc  21533  1stcrest  21535  lly1stc  21578  isref  21591  islocfin  21599  tx1stc  21732  isust  22285  iscfilu  22370  met1stc  22604  iscfil  23341  isgrpo  27742  chne0  28743  pstmfval  30320  dya2iocuni  30726  noetalem3  32240  altxpeq1  32455  altxpeq2  32456  elhf2  32657  bj-sngleq  33314  cover2g  33864  indexdom  33884  istotbnd  33922  pmapglb2xN  35660  paddval  35686  elpadd0  35697  diophrex  37949  hbtlem1  38302  hbtlem7  38304  sprval  42330  sprsymrelfvlem  42341  sprsymrelfv  42345  sprsymrelfo  42348
  Copyright terms: Public domain W3C validator