Theorem rspcedvdw 3579

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061

This theorem is referenced by:  prproe  4861  frxp2  8086  elpq  12888  reltre  13256  rpltrp  13257  reltxrnmnf  13258  modmuladd  13836  modmuladdnn0  13838  ghmqusnsglem1  19209  opprring  20283  pzriprnglem7  21442  pzriprnglem13  21448  pzriprnglem14  21449  pzriprngALT  21450  negleft  28054  negright  28055  oncutlt  28260  oniso  28267  n0fincut  28351  bdayn0sf1o  28366  dfnns2  28368  nohalf  28420  pw2recs  28434  z12negscl  28474  z12sge0  28479  remulscllem1  28496  remulscllem2  28497  2exple2exp  32926  mndlrinvb  33107  mndlactfo  33109  mndractfo  33111  mndlactf1o  33112  mndractf1o  33113  gsumwrd2dccatlem  33159  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem3  33326  elrgspnsubrunlem1  33329  elrgspnsubrunlem2  33330  fracerl  33388  fracfld  33390  idomsubr  33391  dvdsruasso2  33467  unitmulrprm  33609  1arithidomlem1  33616  1arithidom  33618  1arithufdlem1  33625  1arithufdlem2  33626  1arithufdlem3  33627  1arithufdlem4  33628  dfufd2lem  33630  zringfrac  33635  evl1deg1  33657  evl1deg2  33658  evl1deg3  33659  esplyfv1  33727  ply1degltdimlem  33779  fldextrspunlsp  33831  minplyelirng  33872  irredminply  33873  algextdeglem4  33877  algextdeglem8  33881  rtelextdg2lem  33883  fldext2chn  33885  constrmon  33901  constrextdg2lem  33905  constrextdg2  33906  r1filimi  35259  sn-negex12  42672  rediveud  42698  fsuppind  42833  prjspertr  42848  prjsperref  42849  prjspersym  42850  prjspvs  42853  0prjspnrel  42870  flt4lem2  42890  flt4lem7  42902  isuspgrim0lem  48139  uhgrimisgrgriclem  48176  clnbgrgrim  48180  stgrnbgr0  48210  isubgr3stgrlem4  48215  uspgrlimlem2  48235  gpgedgvtx1  48308  gpgprismgr4cycllem3  48343  pgnbgreunbgr  48371  slotresfo  49144  exbaspos  49221  exbasprs  49222  oppff1o  49394  imaid  49399  diag1f1o  49779  diag2f1o  49782