Theorem rexeqdv 3291

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

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

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 2701

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

This theorem is referenced by:  rexeqtrdv  3293  rexeqtrrdv  3295  rexeqbidva  3297  fnunirn  7194  oarec  8487  fival  9321  marypha1lem  9342  marypha1  9343  wemapwe  9612  scshwfzeqfzo  14751  supcvg  15781  zprod  15862  vdwlem6  16916  rami  16945  cshws0  17031  imasleval  17463  isssc  17745  fullestrcsetc  18075  fullsetcestrc  18090  ipodrsfi  18463  grppropd  18848  sylow1lem2  19496  sylow3lem1  19524  lsmass  19566  pj1fval  19591  efgrelexlema  19646  pgpfac1lem2  19974  pgpfac1lem3  19976  pgpfac1lem4  19977  dvdsrval  20264  dvdsrpropd  20319  elrspsn  21165  znunit  21488  ellspd  21727  cnpfval  23137  cmpcov  23292  cmpsublem  23302  cmpsub  23303  tgcmp  23304  uncmp  23306  hauscmplem  23309  1stcfb  23348  llyi  23377  nllyi  23378  cldllycmp  23398  ptrescn  23542  isufl  23816  fmid  23863  alexsublem  23947  alexsubb  23949  alexsubALTlem4  23953  alexsubALT  23954  cnextfres1  23971  tsmsf1o  24048  utopval  24136  imasf1oxms  24393  bndth  24873  ovolicc2  25439  ellimc2  25794  limcflf  25798  plyval  26114  aannenlem1  26252  aannenlem2  26253  ulm2  26310  elmade2  27800  elntg2  28948  uhgrvtxedgiedgb  29099  nb3grprlem2  29344  cplgrop  29400  cusgrexi  29406  structtocusgr  29409  1egrvtxdg0  29475  erclwwlknsym  30032  erclwwlkntr  30033  hashecclwwlkn1  30039  umgrhashecclwwlk  30040  nfrgr2v  30234  isplig  30438  pjhth  31355  pjhfval  31358  pjhtheu2  31378  lsmssass  33352  0ringirng  33663  iscref  33813  crefeq  33814  issros  34144  eulerpartlemgh  34348  onvf1odlem2  35079  onvf1odlem4  35081  ispconn  35198  satfv1  35338  satfvsucsuc  35340  br8  35731  br6  35732  br4  35733  wsuclem  35801  brsegle  36084  hilbert1.1  36130  limsucncmpi  36421  pibt2  37393  poimirlem24  37626  poimirlem25  37627  poimirlem27  37629  poimirlem28  37630  volsupnfl  37647  isgrpda  37937  isdrngo2  37940  lcvfbr  39001  pointsetN  39723  dia1dim2  41044  dib1dim2  41150  diclspsn  41176  dih1dimatlem  41311  lcfrvalsnN  41523  mapdpglem3  41657  mapdpglem26  41680  mapdpglem27  41681  prjspnerlem  42593  0prjspn  42604  isnacs  42680  eldioph  42734  islssfg  43046  itgoval  43137  uzubioo2  45552  limsupre3uzlem  45720  limsupre3uz  45721  limsupreuz  45722  limsupreuzmpt  45724  liminflelimsuplem  45760  liminflelimsup  45761  liminfreuz  45788  stoweidlem50  46035  stoweidlem57  46042  iccelpart  47421  fargshiftfo  47430  stgrfv  47941  gpgov  48030  lco0  48416  iscnrm3r  48936