Theorem rspcedvdw 3577

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

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

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059

This theorem is referenced by:  prproe  4859  frxp2  8084  elpq  12886  reltre  13254  rpltrp  13255  reltxrnmnf  13256  modmuladd  13834  modmuladdnn0  13836  ghmqusnsglem1  19207  opprring  20281  pzriprnglem7  21440  pzriprnglem13  21446  pzriprnglem14  21447  pzriprngALT  21448  negsleft  28027  negsright  28028  onscutlt  28232  onsiso  28236  n0sfincut  28315  bdayn0sf1o  28328  dfnns2  28330  nohalf  28382  pw2recs  28396  zs12negscl  28427  zs12ge0  28432  remulscllem1  28445  remulscllem2  28446  2exple2exp  32875  mndlrinvb  33056  mndlactfo  33058  mndractfo  33060  mndlactf1o  33061  mndractf1o  33062  gsumwrd2dccatlem  33108  elrgspnlem1  33273  elrgspnlem2  33274  elrgspnlem3  33275  elrgspnsubrunlem1  33278  elrgspnsubrunlem2  33279  fracerl  33337  fracfld  33339  idomsubr  33340  dvdsruasso2  33416  unitmulrprm  33558  1arithidomlem1  33565  1arithidom  33567  1arithufdlem1  33574  1arithufdlem2  33575  1arithufdlem3  33576  1arithufdlem4  33577  dfufd2lem  33579  zringfrac  33584  evl1deg1  33606  evl1deg2  33607  evl1deg3  33608  esplyfv1  33676  ply1degltdimlem  33728  fldextrspunlsp  33780  minplyelirng  33821  irredminply  33822  algextdeglem4  33826  algextdeglem8  33830  rtelextdg2lem  33832  fldext2chn  33834  constrmon  33850  constrextdg2lem  33854  constrextdg2  33855  r1filimi  35208  sn-negex12  42614  rediveud  42640  fsuppind  42775  prjspertr  42790  prjsperref  42791  prjspersym  42792  prjspvs  42795  0prjspnrel  42812  flt4lem2  42832  flt4lem7  42844  isuspgrim0lem  48081  uhgrimisgrgriclem  48118  clnbgrgrim  48122  stgrnbgr0  48152  isubgr3stgrlem4  48157  uspgrlimlem2  48177  gpgedgvtx1  48250  gpgprismgr4cycllem3  48285  pgnbgreunbgr  48313  slotresfo  49086  exbaspos  49163  exbasprs  49164  oppff1o  49336  imaid  49341  diag1f1o  49721  diag2f1o  49724