Theorem rspcedvdw 3594

Description: Version of rspcedvd 3593 where the implicit substitution hypothesis does not have an antecedent, which also avoids a disjoint variable condition on 𝜑, 𝑥. (Contributed by SN, 20-Aug-2024.)

Hypotheses

Ref	Expression
rspcedvdw.s	⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))
rspcedvdw.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
rspcedvdw.2	⊢ (𝜑 → 𝜒)

Assertion

Ref	Expression
rspcedvdw	⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜒,𝑥

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

Proof of Theorem rspcedvdw

Step	Hyp	Ref	Expression
1		rspcedvdw.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		rspcedvdw.2	. 2 ⊢ (𝜑 → 𝜒)
3		rspcedvdw.s	. . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))
4	3	rspcev 3591	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜒) → ∃𝑥 ∈ 𝐵 𝜓)
5	1, 2, 4	syl2anc 584	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∃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-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055

This theorem is referenced by:  prproe  4872  frxp2  8126  elpq  12941  reltre  13308  rpltrp  13309  reltxrnmnf  13310  modmuladd  13885  modmuladdnn0  13887  ghmqusnsglem1  19219  opprring  20263  pzriprnglem7  21404  pzriprnglem13  21410  pzriprnglem14  21411  pzriprngALT  21412  onscutlt  28172  onsiso  28176  n0sfincut  28253  bdayn0sf1o  28266  dfnns2  28268  nohalf  28317  pw2recs  28330  zs12negscl  28347  zs12ge0  28349  remulscllem1  28358  remulscllem2  28359  2exple2exp  32777  mndlrinvb  32973  mndlactfo  32975  mndractfo  32977  mndlactf1o  32978  mndractf1o  32979  gsumwrd2dccatlem  33013  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem3  33202  elrgspnsubrunlem1  33205  elrgspnsubrunlem2  33206  fracerl  33263  fracfld  33265  idomsubr  33266  dvdsruasso2  33364  unitmulrprm  33506  1arithidomlem1  33513  1arithidom  33515  1arithufdlem1  33522  1arithufdlem2  33523  1arithufdlem3  33524  1arithufdlem4  33525  dfufd2lem  33527  zringfrac  33532  evl1deg1  33552  evl1deg2  33553  evl1deg3  33554  ply1degltdimlem  33625  fldextrspunlsp  33676  minplyelirng  33712  irredminply  33713  algextdeglem4  33717  algextdeglem8  33721  rtelextdg2lem  33723  fldext2chn  33725  constrmon  33741  constrextdg2lem  33745  constrextdg2  33746  sn-negex12  42412  rediveud  42438  fsuppind  42585  prjspertr  42600  prjsperref  42601  prjspersym  42602  prjspvs  42605  0prjspnrel  42622  flt4lem2  42642  flt4lem7  42654  isuspgrim0lem  47897  uhgrimisgrgriclem  47934  clnbgrgrim  47938  stgrnbgr0  47967  isubgr3stgrlem4  47972  uspgrlimlem2  47992  gpgedgvtx1  48057  gpgprismgr4cycllem3  48091  pgnbgreunbgr  48119  slotresfo  48891  exbaspos  48968  exbasprs  48969  oppff1o  49142  imaid  49147  diag1f1o  49527  diag2f1o  49530