Theorem rspcedvdw 3591

Description: Version of rspcedvd 3590 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 3588	. 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  4869  frxp2  8123  elpq  12934  reltre  13301  rpltrp  13302  reltxrnmnf  13303  modmuladd  13878  modmuladdnn0  13880  ghmqusnsglem1  19212  opprring  20256  pzriprnglem7  21397  pzriprnglem13  21403  pzriprnglem14  21404  pzriprngALT  21405  onscutlt  28165  onsiso  28169  n0sfincut  28246  bdayn0sf1o  28259  dfnns2  28261  nohalf  28310  pw2recs  28323  zs12negscl  28340  zs12ge0  28342  remulscllem1  28351  remulscllem2  28352  2exple2exp  32770  mndlrinvb  32966  mndlactfo  32968  mndractfo  32970  mndlactf1o  32971  mndractf1o  32972  gsumwrd2dccatlem  33006  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem3  33195  elrgspnsubrunlem1  33198  elrgspnsubrunlem2  33199  fracerl  33256  fracfld  33258  idomsubr  33259  dvdsruasso2  33357  unitmulrprm  33499  1arithidomlem1  33506  1arithidom  33508  1arithufdlem1  33515  1arithufdlem2  33516  1arithufdlem3  33517  1arithufdlem4  33518  dfufd2lem  33520  zringfrac  33525  evl1deg1  33545  evl1deg2  33546  evl1deg3  33547  ply1degltdimlem  33618  fldextrspunlsp  33669  minplyelirng  33705  irredminply  33706  algextdeglem4  33710  algextdeglem8  33714  rtelextdg2lem  33716  fldext2chn  33718  constrmon  33734  constrextdg2lem  33738  constrextdg2  33739  sn-negex12  42405  rediveud  42431  fsuppind  42578  prjspertr  42593  prjsperref  42594  prjspersym  42595  prjspvs  42598  0prjspnrel  42615  flt4lem2  42635  flt4lem7  42647  isuspgrim0lem  47893  uhgrimisgrgriclem  47930  clnbgrgrim  47934  stgrnbgr0  47963  isubgr3stgrlem4  47968  uspgrlimlem2  47988  gpgedgvtx1  48053  gpgprismgr4cycllem3  48087  pgnbgreunbgr  48115  slotresfo  48887  exbaspos  48964  exbasprs  48965  oppff1o  49138  imaid  49143  diag1f1o  49523  diag2f1o  49526