Theorem rspcedvdw 3602

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539   ∈ wcel 2107  ∃wrex 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060

This theorem is referenced by:  prproe  4878  frxp2  8137  elpq  12983  reltre  13348  rpltrp  13349  reltxrnmnf  13350  modmuladd  13920  modmuladdnn0  13922  ghmqusnsglem1  19248  opprring  20292  pzriprnglem7  21433  pzriprnglem13  21439  pzriprnglem14  21440  pzriprngALT  21441  dfnns2  28265  remulscllem1  28335  remulscllem2  28336  2exple2exp  32744  mndlrinvb  32939  mndlactfo  32941  mndractfo  32943  mndlactf1o  32944  mndractf1o  32945  gsumwrd2dccatlem  32978  elrgspnlem1  33155  elrgspnlem2  33156  elrgspnlem3  33157  elrgspnsubrunlem1  33160  elrgspnsubrunlem2  33161  fracerl  33218  fracfld  33220  idomsubr  33221  dvdsruasso2  33319  unitmulrprm  33461  1arithidomlem1  33468  1arithidom  33470  1arithufdlem1  33477  1arithufdlem2  33478  1arithufdlem3  33479  1arithufdlem4  33480  dfufd2lem  33482  zringfrac  33487  evl1deg1  33506  evl1deg2  33507  evl1deg3  33508  ply1degltdimlem  33578  fldextrspunlsp  33631  minplyelirng  33665  irredminply  33666  algextdeglem4  33670  algextdeglem8  33674  rtelextdg2lem  33676  fldext2chn  33678  constrmon  33694  constrextdg2lem  33698  constrextdg2  33699  sn-negex12  42384  fsuppind  42538  prjspertr  42553  prjsperref  42554  prjspersym  42555  prjspvs  42558  0prjspnrel  42575  flt4lem2  42595  flt4lem7  42607  isuspgrim0lem  47816  uhgrimisgrgriclem  47843  clnbgrgrim  47847  stgrnbgr0  47876  isubgr3stgrlem4  47881  uspgrlimlem2  47901  gpgedgvtx1  47965  slotresfo  48752  exbaspos  48829  exbasprs  48830  diag1f1o  49204  diag2f1o  49207