Theorem rspcedvdw 3567

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062

This theorem is referenced by:  rspceb2dv  3568  prproe  4848  frxp2  8094  elpq  12925  reltre  13293  rpltrp  13294  reltxrnmnf  13295  modmuladd  13875  modmuladdnn0  13877  ghmqusnsglem1  19255  opprring  20327  pzriprnglem7  21467  pzriprnglem13  21473  pzriprnglem14  21474  pzriprngALT  21475  negleft  28050  negright  28051  oncutlt  28256  oniso  28263  n0fincut  28347  bdayn0sf1o  28362  dfnns2  28364  nohalf  28416  pw2recs  28430  z12negscl  28470  z12sge0  28475  remulscllem1  28492  remulscllem2  28493  2exple2exp  32918  mndlrinvb  33085  mndlactfo  33087  mndractfo  33089  mndlactf1o  33090  mndractf1o  33091  gsumwrd2dccatlem  33138  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem3  33305  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  fracerl  33367  fracfld  33369  idomsubr  33370  dvdsruasso2  33446  unitmulrprm  33588  1arithidomlem1  33595  1arithidom  33597  1arithufdlem1  33604  1arithufdlem2  33605  1arithufdlem3  33606  1arithufdlem4  33607  dfufd2lem  33609  zringfrac  33614  evl1deg1  33636  evl1deg2  33637  evl1deg3  33638  esplyfv1  33713  ply1degltdimlem  33766  fldextrspunlsp  33818  minplyelirng  33859  irredminply  33860  algextdeglem4  33864  algextdeglem8  33868  rtelextdg2lem  33870  fldext2chn  33872  constrmon  33888  constrextdg2lem  33892  constrextdg2  33893  r1filimi  35246  qdiff  37641  sn-negex12  42849  rediveud  42875  fsuppind  43023  prjspertr  43038  prjsperref  43039  prjspersym  43040  prjspvs  43043  0prjspnrel  43060  flt4lem2  43080  flt4lem7  43092  isuspgrim0lem  48369  uhgrimisgrgriclem  48406  clnbgrgrim  48410  stgrnbgr0  48440  isubgr3stgrlem4  48445  uspgrlimlem2  48465  gpgedgvtx1  48538  gpgprismgr4cycllem3  48573  pgnbgreunbgr  48601  slotresfo  49374  exbaspos  49451  exbasprs  49452  oppff1o  49624  imaid  49629  diag1f1o  50009  diag2f1o  50012