Theorem rspcedvdw 3581

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063

This theorem is referenced by:  prproe  4863  frxp2  8096  elpq  12900  reltre  13268  rpltrp  13269  reltxrnmnf  13270  modmuladd  13848  modmuladdnn0  13850  ghmqusnsglem1  19221  opprring  20295  pzriprnglem7  21454  pzriprnglem13  21460  pzriprnglem14  21461  pzriprngALT  21462  negleft  28066  negright  28067  oncutlt  28272  oniso  28279  n0fincut  28363  bdayn0sf1o  28378  dfnns2  28380  nohalf  28432  pw2recs  28446  z12negscl  28486  z12sge0  28491  remulscllem1  28508  remulscllem2  28509  2exple2exp  32937  mndlrinvb  33118  mndlactfo  33120  mndractfo  33122  mndlactf1o  33123  mndractf1o  33124  gsumwrd2dccatlem  33171  elrgspnlem1  33336  elrgspnlem2  33337  elrgspnlem3  33338  elrgspnsubrunlem1  33341  elrgspnsubrunlem2  33342  fracerl  33400  fracfld  33402  idomsubr  33403  dvdsruasso2  33479  unitmulrprm  33621  1arithidomlem1  33628  1arithidom  33630  1arithufdlem1  33637  1arithufdlem2  33638  1arithufdlem3  33639  1arithufdlem4  33640  dfufd2lem  33642  zringfrac  33647  evl1deg1  33669  evl1deg2  33670  evl1deg3  33671  esplyfv1  33746  ply1degltdimlem  33800  fldextrspunlsp  33852  minplyelirng  33893  irredminply  33894  algextdeglem4  33898  algextdeglem8  33902  rtelextdg2lem  33904  fldext2chn  33906  constrmon  33922  constrextdg2lem  33926  constrextdg2  33927  r1filimi  35280  sn-negex12  42787  rediveud  42813  fsuppind  42948  prjspertr  42963  prjsperref  42964  prjspersym  42965  prjspvs  42968  0prjspnrel  42985  flt4lem2  43005  flt4lem7  43017  isuspgrim0lem  48253  uhgrimisgrgriclem  48290  clnbgrgrim  48294  stgrnbgr0  48324  isubgr3stgrlem4  48329  uspgrlimlem2  48349  gpgedgvtx1  48422  gpgprismgr4cycllem3  48457  pgnbgreunbgr  48485  slotresfo  49258  exbaspos  49335  exbasprs  49336  oppff1o  49508  imaid  49513  diag1f1o  49893  diag2f1o  49896