Theorem rexeqdv 3297

Description: Equality deduction for restricted existential quantifier. (Contributed by NM, 14-Jan-2007.)

Hypothesis

Ref	Expression
raleqdv.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
rexeqdv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem rexeqdv

Step	Hyp	Ref	Expression
1		raleqdv.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		rexeq 3292	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))
3	1, 2	syl 17	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-rex 3061

This theorem is referenced by:  rexeqtrdv  3299  rexeqtrrdv  3301  rexeqbidva  3303  fnunirn  7199  oarec  8489  fival  9315  marypha1lem  9336  marypha1  9337  wemapwe  9606  scshwfzeqfzo  14749  supcvg  15779  zprod  15860  vdwlem6  16914  rami  16943  cshws0  17029  imasleval  17462  isssc  17744  fullestrcsetc  18074  fullsetcestrc  18089  ipodrsfi  18462  grppropd  18881  sylow1lem2  19528  sylow3lem1  19556  lsmass  19598  pj1fval  19623  efgrelexlema  19678  pgpfac1lem2  20006  pgpfac1lem3  20008  pgpfac1lem4  20009  dvdsrval  20297  dvdsrpropd  20352  elrspsn  21195  znunit  21518  ellspd  21757  cnpfval  23178  cmpcov  23333  cmpsublem  23343  cmpsub  23344  tgcmp  23345  uncmp  23347  hauscmplem  23350  1stcfb  23389  llyi  23418  nllyi  23419  cldllycmp  23439  ptrescn  23583  isufl  23857  fmid  23904  alexsublem  23988  alexsubb  23990  alexsubALTlem4  23994  alexsubALT  23995  cnextfres1  24012  tsmsf1o  24089  utopval  24176  imasf1oxms  24433  bndth  24913  ovolicc2  25479  ellimc2  25834  limcflf  25838  plyval  26154  aannenlem1  26292  aannenlem2  26293  ulm2  26350  elmade2  27854  elntg2  29058  uhgrvtxedgiedgb  29209  nb3grprlem2  29454  cplgrop  29510  cusgrexi  29516  structtocusgr  29519  1egrvtxdg0  29585  erclwwlknsym  30145  erclwwlkntr  30146  hashecclwwlkn1  30152  umgrhashecclwwlk  30153  nfrgr2v  30347  isplig  30551  pjhth  31468  pjhfval  31471  pjhtheu2  31491  lsmssass  33483  0ringirng  33846  iscref  34001  crefeq  34002  issros  34332  eulerpartlemgh  34535  onvf1odlem2  35298  onvf1odlem4  35300  ispconn  35417  satfv1  35557  satfvsucsuc  35559  br8  35950  br6  35951  br4  35952  wsuclem  36017  brsegle  36302  hilbert1.1  36348  limsucncmpi  36639  pibt2  37622  poimirlem24  37845  poimirlem25  37846  poimirlem27  37848  poimirlem28  37849  volsupnfl  37866  isgrpda  38156  isdrngo2  38159  lcvfbr  39280  pointsetN  40001  dia1dim2  41322  dib1dim2  41428  diclspsn  41454  dih1dimatlem  41589  lcfrvalsnN  41801  mapdpglem3  41935  mapdpglem26  41958  mapdpglem27  41959  prjspnerlem  42860  0prjspn  42871  isnacs  42946  eldioph  43000  islssfg  43312  itgoval  43403  uzubioo2  45813  limsupre3uzlem  45979  limsupre3uz  45980  limsupreuz  45981  limsupreuzmpt  45983  liminflelimsuplem  46019  liminflelimsup  46020  liminfreuz  46047  stoweidlem50  46294  stoweidlem57  46301  iccelpart  47679  fargshiftfo  47688  stgrfv  48199  gpgov  48288  lco0  48673  iscnrm3r  49193