Theorem rspcedvdw 3565

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548   ∈ wcel 2121  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066

This theorem is referenced by:  rspceb2dv  3566  prproe  4839  frxp2  8088  elpq  12920  reltre  13288  rpltrp  13289  reltxrnmnf  13290  modmuladd  13870  modmuladdnn0  13872  ghmqusnsglem1  19250  opprring  20322  pzriprnglem7  21466  pzriprnglem13  21472  pzriprnglem14  21473  pzriprngALT  21474  negleft  28072  negright  28073  oncutlt  28278  oniso  28285  n0fincut  28369  bdayn0sf1o  28384  dfnns2  28386  nohalf  28438  pw2recs  28452  z12negscl  28492  z12sge0  28497  remulscllem1  28514  remulscllem2  28515  2exple2exp  32941  mndlrinvb  33108  mndlactfo  33110  mndractfo  33112  mndlactf1o  33113  mndractf1o  33114  gsumwrd2dccatlem  33162  elrgspnlem1  33327  elrgspnlem2  33328  elrgspnlem3  33329  elrgspnsubrunlem1  33332  elrgspnsubrunlem2  33333  fracerl  33394  fracfld  33396  idomsubr  33397  dvdsruasso2  33473  mxidlirredi  33558  unitmulrprm  33623  1arithidomlem1  33630  1arithidom  33632  1arithufdlem1  33639  1arithufdlem2  33640  1arithufdlem3  33641  1arithufdlem4  33642  dfufd2lem  33644  zringfrac  33649  evl1deg1  33671  evl1deg2  33672  evl1deg3  33673  esplyfv1  33765  ply1degltdimlem  33818  fldextrspunlsp  33870  minplyelirng  33911  irredminply  33912  algextdeglem4  33916  algextdeglem8  33920  rtelextdg2lem  33922  fldext2chn  33924  constrmon  33940  constrextdg2lem  33944  constrextdg2  33945  r1filimi  35299  qdiff  37702  sn-negex12  42909  rediveud  42935  fsuppind  43055  prjspertr  43070  prjsperref  43071  prjspersym  43072  prjspvs  43075  0prjspnrel  43092  flt4lem2  43112  flt4lem7  43124  isuspgrim0lem  48398  uhgrimisgrgriclem  48435  clnbgrgrim  48439  stgrnbgr0  48469  isubgr3stgrlem4  48474  uspgrlimlem2  48494  gpgedgvtx1  48567  gpgprismgr4cycllem3  48602  pgnbgreunbgr  48630  slotresfo  49403  exbaspos  49480  exbasprs  49481  oppff1o  49653  imaid  49658  diag1f1o  50038  diag2f1o  50041