Theorem rexeq 3270

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 2894	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2894	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	rexeqf 3266	1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1624  ∃wrex 3043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-cleq 2745  df-clel 2748  df-nfc 2883  df-rex 3048

This theorem is referenced by:  rexeqi  3274  rexeqdv  3276  rexeqbi1dv  3278  unieq  4588  exss  5072  qseq1  7955  1sdom  8320  pssnn  8335  indexfi  8431  supeq1  8508  bnd2  8921  dfac2b  9135  dfac2OLD  9137  cflem  9252  cflecard  9259  cfeq0  9262  cfsuc  9263  cfflb  9265  cofsmo  9275  elwina  9692  eltskg  9756  rankcf  9783  elnp  9993  elnpi  9994  genpv  10005  xrsupsslem  12322  xrinfmsslem  12323  xrsupss  12324  xrinfmss  12325  hashge2el2difr  13447  isdrs  17127  isipodrs  17354  neifval  21097  ishaus  21320  2ndc1stc  21448  1stcrest  21450  lly1stc  21493  isref  21506  islocfin  21514  tx1stc  21647  isust  22200  iscfilu  22285  met1stc  22519  iscfil  23255  isgrpo  27652  chne0  28654  pstmfval  30240  dya2iocuni  30646  noetalem3  32163  altxpeq1  32378  altxpeq2  32379  elhf2  32580  bj-sngleq  33253  cover2g  33814  indexdom  33834  istotbnd  33873  pmapglb2xN  35553  paddval  35579  elpadd0  35590  diophrex  37833  hbtlem1  38187  hbtlem7  38189  sprval  42231  sprsymrelfvlem  42242  sprsymrelfv  42246  sprsymrelfo  42249