Theorem rexeq 3139

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

Step	Hyp	Ref	Expression
1		nfcv 2764	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2764	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	rexeqf 3135	1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483  ∃wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918

This theorem is referenced by:  rexeqi  3143  rexeqdv  3145  rexeqbi1dv  3147  unieq  4444  exss  4931  qseq1  7796  1sdom  8163  pssnn  8178  indexfi  8274  supeq1  8351  bnd2  8756  dfac2  8953  cflem  9068  cflecard  9075  cfeq0  9078  cfsuc  9079  cfflb  9081  cofsmo  9091  elwina  9508  eltskg  9572  rankcf  9599  elnp  9809  elnpi  9810  genpv  9821  xrsupsslem  12137  xrinfmsslem  12138  xrsupss  12139  xrinfmss  12140  hashge2el2difr  13263  isdrs  16934  isipodrs  17161  neifval  20903  ishaus  21126  2ndc1stc  21254  1stcrest  21256  lly1stc  21299  isref  21312  islocfin  21320  tx1stc  21453  isust  22007  iscfilu  22092  met1stc  22326  iscfil  23063  isgrpo  27351  chne0  28353  pstmfval  29939  dya2iocuni  30345  noetalem3  31865  altxpeq1  32080  altxpeq2  32081  elhf2  32282  bj-sngleq  32955  cover2g  33509  indexdom  33529  istotbnd  33568  pmapglb2xN  35058  paddval  35084  elpadd0  35095  diophrex  37339  hbtlem1  37693  hbtlem7  37695  sprval  41729  sprsymrelfvlem  41740  sprsymrelfv  41744  sprsymrelfo  41747