Theorem rspcedvdw 3593

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096

This theorem is referenced by:  rspceb2dv  3594  prproe  4874  frxp2  8139  elpq  12998  reltre  13366  rpltrp  13367  reltxrnmnf  13368  modmuladd  13948  modmuladdnn0  13950  ghmqusnsglem1  19349  opprring  20428  pzriprnglem7  21605  pzriprnglem13  21611  pzriprnglem14  21612  pzriprngALT  21613  negleft  28216  negright  28217  oncutlt  28422  oniso  28429  n0fincut  28513  bdayn0sf1o  28528  dfnns2  28530  nohalf  28582  pw2recs  28596  z12negscl  28636  z12sge0  28641  remulscllem1  28658  remulscllem2  28659  tglnpt2  28887  plngrotlem1  29026  lnssplnglem  29030  lnssplng  29031  prlngd  29143  prlngex  29153  2exple2exp  33118  mndlrinvb  33285  mndlactfo  33287  mndractfo  33289  mndlactf1o  33290  mndractf1o  33291  gsumwrd2dccatlem  33337  elrgspnlem1  33502  elrgspnlem2  33503  elrgspnlem3  33504  elrgspnsubrunlem1  33507  elrgspnsubrunlem2  33508  rlocinvunit  33535  fracerl  33569  fracfld  33571  idomsubr  33572  dvdsruasso2  33642  mxidlirredi  33698  unitmulrprm  33762  1arithidomlem1  33769  1arithidom  33771  1arithufdlem1  33778  1arithufdlem2  33779  1arithufdlem3  33780  1arithufdlem4  33781  dfufd2lem  33783  zringfrac  33788  evl1deg1  33810  evl1deg2  33811  evl1deg3  33812  esplyfv1  33903  ply1degltdimlem  33956  fldextrspunlsp  34008  minplyelirng  34049  irredminply  34050  algextdeglem4  34054  algextdeglem8  34058  rtelextdg2lem  34060  fldext2chn  34062  constrmon  34078  constrextdg2lem  34082  constrextdg2  34083  ballotlem1c  34842  r1filimi  35438  vonf1oonfo  35497  nmulprop  36580  qdiff  37858  sn-negex12  43067  rediveud  43093  fsuppind  43213  prjspertr  43228  prjsperref  43229  prjspersym  43230  prjspvs  43233  0prjspnrel  43250  flt4lem2  43270  flt4lem7  43282  fourierdlem48  46759  fourierdlem49  46760  isuspgrim0lem  48546  uhgrimisgrgriclem  48583  clnbgrgrim  48587  stgrnbgr0  48617  isubgr3stgrlem4  48622  uspgrlimlem2  48642  gpgedgvtx1  48715  gpgprismgr4cycllem3  48750  pgnbgreunbgr  48778  slotresfo  49561  exbaspos  49638  exbasprs  49639  oppff1o  49811  imaid  49816  diag1f1o  50196  diag2f1o  50199