Theorem rexeqdv 3416

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

Hypothesis

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

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

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

Proof of Theorem rexeqdv

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893  df-rex 3144

This theorem is referenced by:  rexeqbidvOLD  3424  rexeqbidva  3426  fnunirn  7011  oarec  8187  fival  8875  marypha1lem  8896  marypha1  8897  wemapwe  9159  zornn0g  9926  scshwfzeqfzo  14187  supcvg  15210  zprod  15290  vdwlem6  16321  rami  16350  cshws0  16434  imasleval  16813  isssc  17089  fullestrcsetc  17400  fullsetcestrc  17415  ipodrsfi  17772  grppropd  18117  sylow1lem2  18723  sylow3lem1  18751  lsmass  18794  pj1fval  18819  efgrelexlema  18874  ablfacrplem  19186  pgpfac1lem2  19196  pgpfac1lem3  19198  pgpfac1lem4  19199  ablfac2  19210  dvdsrval  19394  dvdsrpropd  19445  znunit  20709  ellspd  20945  cnpfval  21841  cmpcov  21996  cmpsublem  22006  cmpsub  22007  tgcmp  22008  uncmp  22010  hauscmplem  22013  1stcfb  22052  2ndcctbss  22062  1stcelcls  22068  llyi  22081  nllyi  22082  cldllycmp  22102  ptrescn  22246  isufl  22520  fmid  22567  alexsublem  22651  alexsubb  22653  alexsubALTlem4  22657  alexsubALT  22658  cnextfres1  22675  tsmsf1o  22752  utopval  22840  imasf1oxms  23098  bndth  23561  ovolicc2  24122  ellimc2  24474  limcflf  24478  plyval  24782  aannenlem1  24916  aannenlem2  24917  ulm2  24972  elntg2  26770  uhgrvtxedgiedgb  26920  nb3grprlem2  27162  cplgrop  27218  cusgrexi  27224  structtocusgr  27227  1egrvtxdg0  27292  wwlksnextsurj  27677  erclwwlknsym  27848  erclwwlkntr  27849  hashecclwwlkn1  27855  umgrhashecclwwlk  27856  nfrgr2v  28050  isplig  28252  pjhth  29169  pjhfval  29172  pjhtheu2  29192  rspsnel  30936  iscref  31108  crefeq  31109  issros  31434  eulerpartlemgh  31636  ballotlemfc0  31750  ballotlemfcc  31751  ispconn  32470  satfv1  32610  satfvsucsuc  32612  br8  32992  br6  32993  br4  32994  wsuclem  33112  brsegle  33569  hilbert1.1  33615  limsucncmpi  33793  pibt2  34697  poimirlem24  34915  poimirlem25  34916  poimirlem27  34918  poimirlem28  34919  volsupnfl  34936  isgrpda  35232  isdrngo2  35235  lcvfbr  36155  lkrlspeqN  36306  pointsetN  36876  dia1dim2  38197  dib1dim2  38303  diclspsn  38329  dih1dimatlem  38464  lcfrvalsnN  38676  mapdpglem3  38810  mapdpglem26  38833  mapdpglem27  38834  prjspnval2  39265  0prjspn  39268  isnacs  39299  eldioph  39353  islssfg  39668  itgoval  39759  uzubioo2  41843  limsupre3uzlem  42014  limsupre3uz  42015  limsupreuz  42016  limsupreuzmpt  42018  liminflelimsuplem  42054  liminflelimsup  42055  liminfreuz  42082  stoweidlem50  42334  stoweidlem57  42341  iccelpart  43592  fargshiftfo  43601  lco0  44481