Theorem rspcedvdw 3568

Description: Version of rspcedvd 3567 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 3565	. 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:  rspceb2dv  3569  prproe  4849  frxp2  8088  elpq  12919  reltre  13287  rpltrp  13288  reltxrnmnf  13289  modmuladd  13869  modmuladdnn0  13871  ghmqusnsglem1  19249  opprring  20321  pzriprnglem7  21480  pzriprnglem13  21486  pzriprnglem14  21487  pzriprngALT  21488  negleft  28067  negright  28068  oncutlt  28273  oniso  28280  n0fincut  28364  bdayn0sf1o  28379  dfnns2  28381  nohalf  28433  pw2recs  28447  z12negscl  28487  z12sge0  28492  remulscllem1  28509  remulscllem2  28510  2exple2exp  32936  mndlrinvb  33103  mndlactfo  33105  mndractfo  33107  mndlactf1o  33108  mndractf1o  33109  gsumwrd2dccatlem  33156  elrgspnlem1  33321  elrgspnlem2  33322  elrgspnlem3  33323  elrgspnsubrunlem1  33326  elrgspnsubrunlem2  33327  fracerl  33385  fracfld  33387  idomsubr  33388  dvdsruasso2  33464  unitmulrprm  33606  1arithidomlem1  33613  1arithidom  33615  1arithufdlem1  33622  1arithufdlem2  33623  1arithufdlem3  33624  1arithufdlem4  33625  dfufd2lem  33627  zringfrac  33632  evl1deg1  33654  evl1deg2  33655  evl1deg3  33656  esplyfv1  33731  ply1degltdimlem  33785  fldextrspunlsp  33837  minplyelirng  33878  irredminply  33879  algextdeglem4  33883  algextdeglem8  33887  rtelextdg2lem  33889  fldext2chn  33891  constrmon  33907  constrextdg2lem  33911  constrextdg2  33912  r1filimi  35265  sn-negex12  42866  rediveud  42892  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