Theorem rspcedvdw 3588

Description: Version of rspcedvd 3587 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 3585	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜒) → ∃𝑥 ∈ 𝐵 𝜓)
5	1, 2, 4	syl2anc 584	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054

This theorem is referenced by:  prproe  4865  frxp2  8100  elpq  12910  reltre  13277  rpltrp  13278  reltxrnmnf  13279  modmuladd  13854  modmuladdnn0  13856  ghmqusnsglem1  19188  opprring  20232  pzriprnglem7  21373  pzriprnglem13  21379  pzriprnglem14  21380  pzriprngALT  21381  onscutlt  28141  onsiso  28145  n0sfincut  28222  bdayn0sf1o  28235  dfnns2  28237  nohalf  28286  pw2recs  28299  zs12negscl  28316  zs12ge0  28318  remulscllem1  28327  remulscllem2  28328  2exple2exp  32743  mndlrinvb  32939  mndlactfo  32941  mndractfo  32943  mndlactf1o  32944  mndractf1o  32945  gsumwrd2dccatlem  32979  elrgspnlem1  33166  elrgspnlem2  33167  elrgspnlem3  33168  elrgspnsubrunlem1  33171  elrgspnsubrunlem2  33172  fracerl  33229  fracfld  33231  idomsubr  33232  dvdsruasso2  33330  unitmulrprm  33472  1arithidomlem1  33479  1arithidom  33481  1arithufdlem1  33488  1arithufdlem2  33489  1arithufdlem3  33490  1arithufdlem4  33491  dfufd2lem  33493  zringfrac  33498  evl1deg1  33518  evl1deg2  33519  evl1deg3  33520  ply1degltdimlem  33591  fldextrspunlsp  33642  minplyelirng  33678  irredminply  33679  algextdeglem4  33683  algextdeglem8  33687  rtelextdg2lem  33689  fldext2chn  33691  constrmon  33707  constrextdg2lem  33711  constrextdg2  33712  sn-negex12  42378  rediveud  42404  fsuppind  42551  prjspertr  42566  prjsperref  42567  prjspersym  42568  prjspvs  42571  0prjspnrel  42588  flt4lem2  42608  flt4lem7  42620  isuspgrim0lem  47866  uhgrimisgrgriclem  47903  clnbgrgrim  47907  stgrnbgr0  47936  isubgr3stgrlem4  47941  uspgrlimlem2  47961  gpgedgvtx1  48026  gpgprismgr4cycllem3  48060  pgnbgreunbgr  48088  slotresfo  48860  exbaspos  48937  exbasprs  48938  oppff1o  49111  imaid  49116  diag1f1o  49496  diag2f1o  49499