Theorem rspcedvdw 3584

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1560   ∈ wcel 2142  ∃wrex 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087

This theorem is referenced by:  rspceb2dv  3585  prproe  4863  frxp2  8124  elpq  12976  reltre  13344  rpltrp  13345  reltxrnmnf  13346  modmuladd  13926  modmuladdnn0  13928  ghmqusnsglem1  19320  opprring  20392  pzriprnglem7  21536  pzriprnglem13  21542  pzriprnglem14  21543  pzriprngALT  21544  negleft  28148  negright  28149  oncutlt  28354  oniso  28361  n0fincut  28445  bdayn0sf1o  28460  dfnns2  28462  nohalf  28514  pw2recs  28528  z12negscl  28568  z12sge0  28573  remulscllem1  28590  remulscllem2  28591  tglnpt2  28819  plngrotlem1  28991  lnssplnglem  28995  lnssplng  28996  prlngd  29063  2exple2exp  33033  mndlrinvb  33200  mndlactfo  33202  mndractfo  33204  mndlactf1o  33205  mndractf1o  33206  gsumwrd2dccatlem  33254  elrgspnlem1  33420  elrgspnlem2  33421  elrgspnlem3  33422  elrgspnsubrunlem1  33425  elrgspnsubrunlem2  33426  rlocinvunit  33453  fracerl  33490  fracfld  33492  idomsubr  33493  dvdsruasso2  33569  mxidlirredi  33656  unitmulrprm  33721  1arithidomlem1  33728  1arithidom  33730  1arithufdlem1  33737  1arithufdlem2  33738  1arithufdlem3  33739  1arithufdlem4  33740  dfufd2lem  33742  zringfrac  33747  evl1deg1  33769  evl1deg2  33770  evl1deg3  33771  esplyfv1  33863  ply1degltdimlem  33916  fldextrspunlsp  33968  minplyelirng  34009  irredminply  34010  algextdeglem4  34014  algextdeglem8  34018  rtelextdg2lem  34020  fldext2chn  34022  constrmon  34038  constrextdg2lem  34042  constrextdg2  34043  ballotlem1c  34802  r1filimi  35396  vonf1oonfo  35455  nmulprop  36537  qdiff  37816  sn-negex12  43023  rediveud  43049  fsuppind  43169  prjspertr  43184  prjsperref  43185  prjspersym  43186  prjspvs  43189  0prjspnrel  43206  flt4lem2  43226  flt4lem7  43238  fourierdlem48  46725  fourierdlem49  46726  isuspgrim0lem  48512  uhgrimisgrgriclem  48549  clnbgrgrim  48553  stgrnbgr0  48583  isubgr3stgrlem4  48588  uspgrlimlem2  48608  gpgedgvtx1  48681  gpgprismgr4cycllem3  48716  pgnbgreunbgr  48744  slotresfo  49517  exbaspos  49594  exbasprs  49595  oppff1o  49767  imaid  49772  diag1f1o  50152  diag2f1o  50155