Theorem rspcedvdw 3625

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071

This theorem is referenced by:  prproe  4905  frxp2  8169  elpq  13017  reltre  13382  rpltrp  13383  reltxrnmnf  13384  modmuladd  13954  modmuladdnn0  13956  ghmqusnsglem1  19298  opprring  20347  pzriprnglem7  21498  pzriprnglem13  21504  pzriprnglem14  21505  pzriprngALT  21506  dfnns2  28362  remulscllem1  28432  remulscllem2  28433  2exple2exp  32834  mndlrinvb  33030  mndlactfo  33032  mndractfo  33034  mndlactf1o  33035  mndractf1o  33036  gsumwrd2dccatlem  33069  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem3  33248  elrgspnsubrunlem1  33251  elrgspnsubrunlem2  33252  fracerl  33308  fracfld  33310  idomsubr  33311  dvdsruasso2  33414  unitmulrprm  33556  1arithidomlem1  33563  1arithidom  33565  1arithufdlem1  33572  1arithufdlem2  33573  1arithufdlem3  33574  1arithufdlem4  33575  dfufd2lem  33577  zringfrac  33582  evl1deg1  33601  evl1deg2  33602  evl1deg3  33603  ply1degltdimlem  33673  fldextrspunlsp  33724  irredminply  33757  algextdeglem4  33761  algextdeglem8  33765  rtelextdg2lem  33767  fldext2chn  33769  constrmon  33785  constrextdg2lem  33789  constrextdg2  33790  sn-negex12  42446  fsuppind  42600  prjspertr  42615  prjsperref  42616  prjspersym  42617  prjspvs  42620  0prjspnrel  42637  flt4lem2  42657  flt4lem7  42669  isuspgrim0lem  47871  uhgrimisgrgriclem  47898  clnbgrgrim  47902  stgrnbgr0  47931  isubgr3stgrlem4  47936  uspgrlimlem2  47956  gpgedgvtx1  48020