Theorem rspcedvdw 3586

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146  ∃wrex 3091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092

This theorem is used by:  rspceb2dv  3587  prproe  4872  frxp2  8146  elpq  13015  reltre  13383  rpltrp  13384  reltxrnmnf  13385  modmuladd  13967  modmuladdnn0  13969  ghmqusnsglem1  19394  opprring  20475  isdrng3lem1  20901  pzriprnglem7  21687  pzriprnglem13  21693  pzriprnglem14  21694  pzriprngALT  21695  negleft  28302  negright  28303  oncutlt  28508  oniso  28515  n0fincut  28599  bdayn0sf1o  28614  dfnns2  28616  nohalf  28668  pw2recs  28682  z12negscl  28722  z12sge0  28727  remulscllem1  28744  remulscllem2  28745  tglnpt2  28977  plngrotlem1  29120  lnssplnglem  29124  lnssplng  29125  prlngd  29244  dfprlng2  29252  prlngex  29256  prlngmo2  29261  2exple2exp  33248  mndlrinvb  33409  mndlactfo  33411  mndractfo  33413  mndlactf1o  33414  mndractf1o  33415  gsumwrd2dccatlem  33461  elrgspnlem1  33626  elrgspnlem2  33627  elrgspnlem3  33628  elrgspnsubrunlem1  33631  elrgspnsubrunlem2  33632  rlocinvunit  33659  fracerl  33691  fracfld  33693  idomsubr  33694  dvdsruasso2  33763  mxidlirredi  33818  unitmulrprm  33882  1arithidomlem1  33889  1arithidom  33891  1arithufdlem1  33898  1arithufdlem2  33899  1arithufdlem3  33900  1arithufdlem4  33901  dfufd2lem  33903  zringfrac  33908  evl1deg1  33930  evl1deg2  33931  evl1deg3  33932  esplyfv1  34023  ply1degltdimlem  34076  fldextrspunlsp  34128  minplyelirng  34169  irredminply  34170  algextdeglem4  34174  algextdeglem8  34178  rtelextdg2lem  34180  fldext2chn  34182  constrmon  34198  constrextdg2lem  34202  constrextdg2  34203  ballotlem1c  34963  r1filimi  35555  vonf1oonfo  35656  nmulprop  36719  qdiff  38028  sn-negex12  43236  rediveud  43262  fsuppind  43380  prjspertr  43395  prjsperref  43396  prjspersym  43397  prjspvs  43400  0prjspnrel  43417  flt4lem2  43437  flt4lem7  43449  fourierdlem48  46926  fourierdlem49  46927  sqrtnzqaa  47663  isuspgrim0lem  48716  uhgrimisgrgriclem  48753  clnbgrgrim  48757  stgrnbgr0  48787  isubgr3stgrlem4  48792  uspgrlimlem2  48812  gpgedgvtx1  48885  gpgprismgr4cycllem3  48920  pgnbgreunbgr  48948  slotresfo  49734  exbaspos  49811  exbasprs  49812  oppff1o  49984  imaid  49989  diag1f1o  50369  diag2f1o  50372