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  19194  opprring  20267  pzriprnglem7  21429  pzriprnglem13  21435  pzriprnglem14  21436  pzriprngALT  21437  onscutlt  28205  onsiso  28209  n0sfincut  28286  bdayn0sf1o  28299  dfnns2  28301  nohalf  28351  pw2recs  28365  zs12negscl  28390  zs12ge0  28395  remulscllem1  28404  remulscllem2  28405  2exple2exp  32820  mndlrinvb  33009  mndlactfo  33011  mndractfo  33013  mndlactf1o  33014  mndractf1o  33015  gsumwrd2dccatlem  33049  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnlem3  33211  elrgspnsubrunlem1  33214  elrgspnsubrunlem2  33215  fracerl  33272  fracfld  33274  idomsubr  33275  dvdsruasso2  33350  unitmulrprm  33492  1arithidomlem1  33499  1arithidom  33501  1arithufdlem1  33508  1arithufdlem2  33509  1arithufdlem3  33510  1arithufdlem4  33511  dfufd2lem  33513  zringfrac  33518  evl1deg1  33538  evl1deg2  33539  evl1deg3  33540  ply1degltdimlem  33611  fldextrspunlsp  33662  minplyelirng  33698  irredminply  33699  algextdeglem4  33703  algextdeglem8  33707  rtelextdg2lem  33709  fldext2chn  33711  constrmon  33727  constrextdg2lem  33731  constrextdg2  33732  sn-negex12  42398  rediveud  42424  fsuppind  42571  prjspertr  42586  prjsperref  42587  prjspersym  42588  prjspvs  42591  0prjspnrel  42608  flt4lem2  42628  flt4lem7  42640  isuspgrim0lem  47886  uhgrimisgrgriclem  47923  clnbgrgrim  47927  stgrnbgr0  47956  isubgr3stgrlem4  47961  uspgrlimlem2  47981  gpgedgvtx1  48046  gpgprismgr4cycllem3  48080  pgnbgreunbgr  48108  slotresfo  48880  exbaspos  48957  exbasprs  48958  oppff1o  49131  imaid  49136  diag1f1o  49516  diag2f1o  49519