Theorem rexeqdv 3322

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 3317	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))
3	1, 2	syl 18	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-rex 3089

This theorem is used by:  rexeqtrdv  3324  rexeqtrrdv  3326  rexeqbidva  3328  fnunirn  7254  oarec  8553  fival  9386  marypha1lem  9407  marypha1  9408  wemapwe  9680  scshwfzeqfzo  14901  supcvg  15949  zprod  16030  vdwlem6  17084  rami  17113  cshws0  17199  imasleval  17633  isssc  17915  fullestrcsetc  18245  fullsetcestrc  18260  ipodrsfi  18633  grppropd  19081  sylow1lem2  19732  sylow3lem1  19760  lsmass  19802  pj1fval  19827  efgrelexlema  19882  pgpfac1lem2  20210  pgpfac1lem3  20212  pgpfac1lem4  20213  dvdsrval  20508  dvdsrpropd  20563  isdrng3lem1  20920  elrspsn  21440  znunit  21782  ellspd  22021  cnpfval  23465  cmpcov  23620  cmpsublem  23630  cmpsub  23631  tgcmp  23632  uncmp  23634  hauscmplem  23637  1stcfb  23676  llyi  23706  nllyi  23707  cldllycmp  23727  ptrescn  23871  isufl  24145  fmid  24192  alexsublem  24276  alexsubb  24278  alexsubALTlem4  24282  alexsubALT  24283  cnextfres1  24300  tsmsf1o  24377  utopval  24464  imasf1oxms  24721  bndth  25192  ovolicc2  25756  ellimc2  26111  limcflf  26115  plyval  26425  aannenlem1  26571  aannenlem2  26572  ulm2  26628  elmade2  28131  tgaaddcpbllem2  29237  brprlng  29303  elntg2  29450  uhgrvtxedgiedgb  29601  nb3grprlem2  29849  cplgrop  29905  cusgrexi  29911  structtocusgr  29914  1egrvtxdg0  29979  erclwwlknsym  30548  erclwwlkntr  30549  hashecclwwlkn1  30555  umgrhashecclwwlk  30556  nfrgr2v  30760  isplig  30965  pjhth  31882  pjhfval  31885  pjhtheu2  31905  lsmssass  33839  0ringirng  34207  iscref  34362  crefeq  34363  issros  34694  eulerpartlemgh  34897  onvf1odlem2  35709  onvf1odlem4  35711  ispconn  35810  satfv1  35950  satfvsucsuc  35952  br8  36343  br6  36344  br4  36345  wsuclem  36410  brsegle  36696  hilbert1.1  36742  limsucncmpi  37072  pibt2  38179  poimirlem24  38401  poimirlem25  38402  poimirlem27  38404  poimirlem28  38405  volsupnfl  38422  isgrpda  38713  isdrngo2  38716  lcvfbr  39901  pointsetN  40622  dia1dim2  41943  dib1dim2  42049  diclspsn  42075  dih1dimatlem  42210  lcfrvalsnN  42422  mapdpglem3  42556  mapdpglem26  42579  mapdpglem27  42580  prjspnerlem  43471  0prjspn  43482  isnacs  43557  eldioph  43611  islssfg  43919  itgoval  44010  uzubioo2  46405  limsupre3uzlem  46571  limsupre3uz  46572  limsupreuz  46573  limsupreuzmpt  46575  liminflelimsuplem  46611  liminflelimsup  46612  liminfreuz  46639  stoweidlem50  46886  stoweidlem57  46893  iccelpart  48341  fargshiftfo  48350  stgrfv  48877  gpgov  48966  lco0  49365  iscnrm3r  49882