Theorem rexeqdv 3327

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

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

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 2156  ax-ext 2738

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

This theorem is used by:  rexeqtrdv  3329  rexeqtrrdv  3331  rexeqbidva  3333  fnunirn  7258  oarec  8556  fival  9382  marypha1lem  9403  marypha1  9404  wemapwe  9676  scshwfzeqfzo  14889  supcvg  15936  zprod  16017  vdwlem6  17071  rami  17100  cshws0  17186  imasleval  17620  isssc  17902  fullestrcsetc  18232  fullsetcestrc  18247  ipodrsfi  18620  grppropd  19049  sylow1lem2  19700  sylow3lem1  19728  lsmass  19770  pj1fval  19795  efgrelexlema  19850  pgpfac1lem2  20178  pgpfac1lem3  20180  pgpfac1lem4  20181  dvdsrval  20476  dvdsrpropd  20531  isdrng3lem1  20888  elrspsn  21408  znunit  21750  ellspd  21989  cnpfval  23428  cmpcov  23583  cmpsublem  23593  cmpsub  23594  tgcmp  23595  uncmp  23597  hauscmplem  23600  1stcfb  23639  llyi  23668  nllyi  23669  cldllycmp  23689  ptrescn  23833  isufl  24107  fmid  24154  alexsublem  24238  alexsubb  24240  alexsubALTlem4  24244  alexsubALT  24245  cnextfres1  24262  tsmsf1o  24339  utopval  24426  imasf1oxms  24683  bndth  25154  ovolicc2  25718  ellimc2  26073  limcflf  26077  plyval  26387  aannenlem1  26528  aannenlem2  26529  ulm2  26585  elmade2  28088  brprlng  29225  elntg2  29372  uhgrvtxedgiedgb  29523  nb3grprlem2  29768  cplgrop  29824  cusgrexi  29830  structtocusgr  29833  1egrvtxdg0  29898  erclwwlknsym  30458  erclwwlkntr  30459  hashecclwwlkn1  30465  umgrhashecclwwlk  30466  nfrgr2v  30660  isplig  30865  pjhth  31782  pjhfval  31785  pjhtheu2  31805  lsmssass  33742  0ringirng  34110  iscref  34265  crefeq  34266  issros  34597  eulerpartlemgh  34800  onvf1odlem2  35612  onvf1odlem4  35614  ispconn  35736  satfv1  35876  satfvsucsuc  35878  br8  36269  br6  36270  br4  36271  wsuclem  36336  brsegle  36621  hilbert1.1  36667  limsucncmpi  36997  pibt2  38104  poimirlem24  38336  poimirlem25  38337  poimirlem27  38339  poimirlem28  38340  volsupnfl  38357  isgrpda  38647  isdrngo2  38650  lcvfbr  39835  pointsetN  40556  dia1dim2  41877  dib1dim2  41983  diclspsn  42009  dih1dimatlem  42144  lcfrvalsnN  42356  mapdpglem3  42490  mapdpglem26  42513  mapdpglem27  42514  prjspnerlem  43390  0prjspn  43401  isnacs  43476  eldioph  43530  islssfg  43838  itgoval  43929  uzubioo2  46324  limsupre3uzlem  46490  limsupre3uz  46491  limsupreuz  46492  limsupreuzmpt  46494  liminflelimsuplem  46530  liminflelimsup  46531  liminfreuz  46558  stoweidlem50  46805  stoweidlem57  46812  iccelpart  48223  fargshiftfo  48232  stgrfv  48759  gpgov  48848  lco0  49248  iscnrm3r  49767