Theorem rspcedvdw 3563

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064

This theorem is referenced by:  rspceb2dv  3564  prproe  4836  frxp2  8084  elpq  12916  reltre  13284  rpltrp  13285  reltxrnmnf  13286  modmuladd  13866  modmuladdnn0  13868  ghmqusnsglem1  19246  opprring  20318  pzriprnglem7  21462  pzriprnglem13  21468  pzriprnglem14  21469  pzriprngALT  21470  negleft  28068  negright  28069  oncutlt  28274  oniso  28281  n0fincut  28365  bdayn0sf1o  28380  dfnns2  28382  nohalf  28434  pw2recs  28448  z12negscl  28488  z12sge0  28493  remulscllem1  28510  remulscllem2  28511  2exple2exp  32937  mndlrinvb  33104  mndlactfo  33106  mndractfo  33108  mndlactf1o  33109  mndractf1o  33110  gsumwrd2dccatlem  33158  elrgspnlem1  33323  elrgspnlem2  33324  elrgspnlem3  33325  elrgspnsubrunlem1  33328  elrgspnsubrunlem2  33329  fracerl  33390  fracfld  33392  idomsubr  33393  dvdsruasso2  33469  unitmulrprm  33611  1arithidomlem1  33618  1arithidom  33620  1arithufdlem1  33627  1arithufdlem2  33628  1arithufdlem3  33629  1arithufdlem4  33630  dfufd2lem  33632  zringfrac  33637  evl1deg1  33659  evl1deg2  33660  evl1deg3  33661  esplyfv1  33753  ply1degltdimlem  33806  fldextrspunlsp  33858  minplyelirng  33899  irredminply  33900  algextdeglem4  33904  algextdeglem8  33908  rtelextdg2lem  33910  fldext2chn  33912  constrmon  33928  constrextdg2lem  33932  constrextdg2  33933  r1filimi  35284  qdiff  37687  sn-negex12  42894  rediveud  42920  fsuppind  43040  prjspertr  43055  prjsperref  43056  prjspersym  43057  prjspvs  43060  0prjspnrel  43077  flt4lem2  43097  flt4lem7  43109  isuspgrim0lem  48384  uhgrimisgrgriclem  48421  clnbgrgrim  48425  stgrnbgr0  48455  isubgr3stgrlem4  48460  uspgrlimlem2  48480  gpgedgvtx1  48553  gpgprismgr4cycllem3  48588  pgnbgreunbgr  48616  slotresfo  49389  exbaspos  49466  exbasprs  49467  oppff1o  49639  imaid  49644  diag1f1o  50024  diag2f1o  50027