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 595	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090

This theorem is referenced by:  rspceb2dv  3585  prproe  4870  frxp2  8136  elpq  12994  reltre  13362  rpltrp  13363  reltxrnmnf  13364  modmuladd  13945  modmuladdnn0  13947  ghmqusnsglem1  19345  opprring  20425  isdrng3lem1  20851  pzriprnglem7  21637  pzriprnglem13  21643  pzriprnglem14  21644  pzriprngALT  21645  negleft  28251  negright  28252  oncutlt  28457  oniso  28464  n0fincut  28548  bdayn0sf1o  28563  dfnns2  28565  nohalf  28617  pw2recs  28631  z12negscl  28671  z12sge0  28676  remulscllem1  28693  remulscllem2  28694  tglnpt2  28926  plngrotlem1  29069  lnssplnglem  29073  lnssplng  29074  prlngd  29189  dfprlng2  29197  prlngex  29201  prlngmo2  29206  2exple2exp  33178  mndlrinvb  33345  mndlactfo  33347  mndractfo  33349  mndlactf1o  33350  mndractf1o  33351  gsumwrd2dccatlem  33397  elrgspnlem1  33562  elrgspnlem2  33563  elrgspnlem3  33564  elrgspnsubrunlem1  33567  elrgspnsubrunlem2  33568  rlocinvunit  33595  fracerl  33627  fracfld  33629  idomsubr  33630  dvdsruasso2  33699  mxidlirredi  33754  unitmulrprm  33818  1arithidomlem1  33825  1arithidom  33827  1arithufdlem1  33834  1arithufdlem2  33835  1arithufdlem3  33836  1arithufdlem4  33837  dfufd2lem  33839  zringfrac  33844  evl1deg1  33866  evl1deg2  33867  evl1deg3  33868  esplyfv1  33959  ply1degltdimlem  34012  fldextrspunlsp  34064  minplyelirng  34105  irredminply  34106  algextdeglem4  34110  algextdeglem8  34114  rtelextdg2lem  34116  fldext2chn  34118  constrmon  34134  constrextdg2lem  34138  constrextdg2  34139  ballotlem1c  34898  r1filimi  35497  vonf1oonfo  35599  nmulprop  36682  qdiff  37971  sn-negex12  43178  rediveud  43204  fsuppind  43322  prjspertr  43337  prjsperref  43338  prjspersym  43339  prjspvs  43342  0prjspnrel  43359  flt4lem2  43379  flt4lem7  43391  fourierdlem48  46868  fourierdlem49  46869  sqrtnzqaa  47605  isuspgrim0lem  48658  uhgrimisgrgriclem  48695  clnbgrgrim  48699  stgrnbgr0  48729  isubgr3stgrlem4  48734  uspgrlimlem2  48754  gpgedgvtx1  48827  gpgprismgr4cycllem3  48862  pgnbgreunbgr  48890  slotresfo  49677  exbaspos  49754  exbasprs  49755  oppff1o  49927  imaid  49932  diag1f1o  50312  diag2f1o  50315