Theorem rspcedvdw 3580

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054

This theorem is referenced by:  prproe  4856  frxp2  8077  elpq  12876  reltre  13243  rpltrp  13244  reltxrnmnf  13245  modmuladd  13820  modmuladdnn0  13822  ghmqusnsglem1  19159  opprring  20232  pzriprnglem7  21394  pzriprnglem13  21400  pzriprnglem14  21401  pzriprngALT  21402  onscutlt  28170  onsiso  28174  n0sfincut  28251  bdayn0sf1o  28264  dfnns2  28266  nohalf  28316  pw2recs  28330  zs12negscl  28355  zs12ge0  28360  remulscllem1  28369  remulscllem2  28370  2exple2exp  32790  mndlrinvb  32979  mndlactfo  32981  mndractfo  32983  mndlactf1o  32984  mndractf1o  32985  gsumwrd2dccatlem  33019  elrgspnlem1  33182  elrgspnlem2  33183  elrgspnlem3  33184  elrgspnsubrunlem1  33187  elrgspnsubrunlem2  33188  fracerl  33245  fracfld  33247  idomsubr  33248  dvdsruasso2  33323  unitmulrprm  33465  1arithidomlem1  33472  1arithidom  33474  1arithufdlem1  33481  1arithufdlem2  33482  1arithufdlem3  33483  1arithufdlem4  33484  dfufd2lem  33486  zringfrac  33491  evl1deg1  33511  evl1deg2  33512  evl1deg3  33513  ply1degltdimlem  33589  fldextrspunlsp  33641  minplyelirng  33682  irredminply  33683  algextdeglem4  33687  algextdeglem8  33691  rtelextdg2lem  33693  fldext2chn  33695  constrmon  33711  constrextdg2lem  33715  constrextdg2  33716  sn-negex12  42390  rediveud  42416  fsuppind  42563  prjspertr  42578  prjsperref  42579  prjspersym  42580  prjspvs  42583  0prjspnrel  42600  flt4lem2  42620  flt4lem7  42632  isuspgrim0lem  47877  uhgrimisgrgriclem  47914  clnbgrgrim  47918  stgrnbgr0  47948  isubgr3stgrlem4  47953  uspgrlimlem2  47973  gpgedgvtx1  48046  gpgprismgr4cycllem3  48081  pgnbgreunbgr  48109  slotresfo  48883  exbaspos  48960  exbasprs  48961  oppff1o  49134  imaid  49139  diag1f1o  49519  diag2f1o  49522