Theorem rexeqdv 3302

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-rex 3055

This theorem is referenced by:  rexeqtrdv  3304  rexeqtrrdv  3306  rexeqbidva  3308  fnunirn  7231  oarec  8529  fival  9370  marypha1lem  9391  marypha1  9392  wemapwe  9657  scshwfzeqfzo  14799  supcvg  15829  zprod  15910  vdwlem6  16964  rami  16993  cshws0  17079  imasleval  17511  isssc  17789  fullestrcsetc  18119  fullsetcestrc  18134  ipodrsfi  18505  grppropd  18890  sylow1lem2  19536  sylow3lem1  19564  lsmass  19606  pj1fval  19631  efgrelexlema  19686  pgpfac1lem2  20014  pgpfac1lem3  20016  pgpfac1lem4  20017  dvdsrval  20277  dvdsrpropd  20332  elrspsn  21157  znunit  21480  ellspd  21718  cnpfval  23128  cmpcov  23283  cmpsublem  23293  cmpsub  23294  tgcmp  23295  uncmp  23297  hauscmplem  23300  1stcfb  23339  llyi  23368  nllyi  23369  cldllycmp  23389  ptrescn  23533  isufl  23807  fmid  23854  alexsublem  23938  alexsubb  23940  alexsubALTlem4  23944  alexsubALT  23945  cnextfres1  23962  tsmsf1o  24039  utopval  24127  imasf1oxms  24384  bndth  24864  ovolicc2  25430  ellimc2  25785  limcflf  25789  plyval  26105  aannenlem1  26243  aannenlem2  26244  ulm2  26301  elmade2  27787  elntg2  28919  uhgrvtxedgiedgb  29070  nb3grprlem2  29315  cplgrop  29371  cusgrexi  29377  structtocusgr  29380  1egrvtxdg0  29446  erclwwlknsym  30006  erclwwlkntr  30007  hashecclwwlkn1  30013  umgrhashecclwwlk  30014  nfrgr2v  30208  isplig  30412  pjhth  31329  pjhfval  31332  pjhtheu2  31352  lsmssass  33380  0ringirng  33691  iscref  33841  crefeq  33842  issros  34172  eulerpartlemgh  34376  onvf1odlem2  35098  onvf1odlem4  35100  ispconn  35217  satfv1  35357  satfvsucsuc  35359  br8  35750  br6  35751  br4  35752  wsuclem  35820  brsegle  36103  hilbert1.1  36149  limsucncmpi  36440  pibt2  37412  poimirlem24  37645  poimirlem25  37646  poimirlem27  37648  poimirlem28  37649  volsupnfl  37666  isgrpda  37956  isdrngo2  37959  lcvfbr  39020  pointsetN  39742  dia1dim2  41063  dib1dim2  41169  diclspsn  41195  dih1dimatlem  41330  lcfrvalsnN  41542  mapdpglem3  41676  mapdpglem26  41699  mapdpglem27  41700  prjspnerlem  42612  0prjspn  42623  isnacs  42699  eldioph  42753  islssfg  43066  itgoval  43157  uzubioo2  45572  limsupre3uzlem  45740  limsupre3uz  45741  limsupreuz  45742  limsupreuzmpt  45744  liminflelimsuplem  45780  liminflelimsup  45781  liminfreuz  45808  stoweidlem50  46055  stoweidlem57  46062  iccelpart  47438  fargshiftfo  47447  stgrfv  47956  gpgov  48037  lco0  48420  iscnrm3r  48940