Theorem rspcedvdw 3604

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  ∃wrex 3060

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061

This theorem is referenced by:  prproe  4881  frxp2  8143  elpq  12991  reltre  13357  rpltrp  13358  reltxrnmnf  13359  modmuladd  13931  modmuladdnn0  13933  ghmqusnsglem1  19263  opprring  20307  pzriprnglem7  21448  pzriprnglem13  21454  pzriprnglem14  21455  pzriprngALT  21456  onscutlt  28217  onsiso  28221  n0sfincut  28298  bdayn0sf1o  28311  dfnns2  28313  nohalf  28362  pw2recs  28375  zs12negscl  28392  zs12ge0  28394  remulscllem1  28403  remulscllem2  28404  2exple2exp  32824  mndlrinvb  33020  mndlactfo  33022  mndractfo  33024  mndlactf1o  33025  mndractf1o  33026  gsumwrd2dccatlem  33060  elrgspnlem1  33237  elrgspnlem2  33238  elrgspnlem3  33239  elrgspnsubrunlem1  33242  elrgspnsubrunlem2  33243  fracerl  33300  fracfld  33302  idomsubr  33303  dvdsruasso2  33401  unitmulrprm  33543  1arithidomlem1  33550  1arithidom  33552  1arithufdlem1  33559  1arithufdlem2  33560  1arithufdlem3  33561  1arithufdlem4  33562  dfufd2lem  33564  zringfrac  33569  evl1deg1  33589  evl1deg2  33590  evl1deg3  33591  ply1degltdimlem  33662  fldextrspunlsp  33715  minplyelirng  33749  irredminply  33750  algextdeglem4  33754  algextdeglem8  33758  rtelextdg2lem  33760  fldext2chn  33762  constrmon  33778  constrextdg2lem  33782  constrextdg2  33783  sn-negex12  42459  fsuppind  42613  prjspertr  42628  prjsperref  42629  prjspersym  42630  prjspvs  42633  0prjspnrel  42650  flt4lem2  42670  flt4lem7  42682  isuspgrim0lem  47906  uhgrimisgrgriclem  47943  clnbgrgrim  47947  stgrnbgr0  47976  isubgr3stgrlem4  47981  uspgrlimlem2  48001  gpgedgvtx1  48066  gpgprismgr4cycllem3  48096  slotresfo  48873  exbaspos  48950  exbasprs  48951  imaid  49094  diag1f1o  49419  diag2f1o  49422