Theorem rspcedvdw 3575

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057

This theorem is referenced by:  prproe  4854  frxp2  8074  elpq  12873  reltre  13240  rpltrp  13241  reltxrnmnf  13242  modmuladd  13820  modmuladdnn0  13822  ghmqusnsglem1  19192  opprring  20265  pzriprnglem7  21424  pzriprnglem13  21430  pzriprnglem14  21431  pzriprngALT  21432  onscutlt  28201  onsiso  28205  n0sfincut  28282  bdayn0sf1o  28295  dfnns2  28297  nohalf  28347  pw2recs  28361  zs12negscl  28388  zs12ge0  28393  remulscllem1  28402  remulscllem2  28403  2exple2exp  32828  mndlrinvb  33006  mndlactfo  33008  mndractfo  33010  mndlactf1o  33011  mndractf1o  33012  gsumwrd2dccatlem  33046  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnlem3  33211  elrgspnsubrunlem1  33214  elrgspnsubrunlem2  33215  fracerl  33272  fracfld  33274  idomsubr  33275  dvdsruasso2  33351  unitmulrprm  33493  1arithidomlem1  33500  1arithidom  33502  1arithufdlem1  33509  1arithufdlem2  33510  1arithufdlem3  33511  1arithufdlem4  33512  dfufd2lem  33514  zringfrac  33519  evl1deg1  33539  evl1deg2  33540  evl1deg3  33541  esplyfv1  33590  ply1degltdimlem  33635  fldextrspunlsp  33687  minplyelirng  33728  irredminply  33729  algextdeglem4  33733  algextdeglem8  33737  rtelextdg2lem  33739  fldext2chn  33741  constrmon  33757  constrextdg2lem  33761  constrextdg2  33762  r1filimi  35114  sn-negex12  42458  rediveud  42484  fsuppind  42631  prjspertr  42646  prjsperref  42647  prjspersym  42648  prjspvs  42651  0prjspnrel  42668  flt4lem2  42688  flt4lem7  42700  isuspgrim0lem  47932  uhgrimisgrgriclem  47969  clnbgrgrim  47973  stgrnbgr0  48003  isubgr3stgrlem4  48008  uspgrlimlem2  48028  gpgedgvtx1  48101  gpgprismgr4cycllem3  48136  pgnbgreunbgr  48164  slotresfo  48938  exbaspos  49015  exbasprs  49016  oppff1o  49189  imaid  49194  diag1f1o  49574  diag2f1o  49577