Theorem rspcedvdw 3579

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087

This theorem is used by:  rspceb2dv  3580  prproe  4865  frxp2  8143  elpq  13026  reltre  13394  rpltrp  13395  reltxrnmnf  13396  modmuladd  13978  modmuladdnn0  13980  ghmqusnsglem1  19408  opprring  20489  isdrng3lem1  20915  pzriprnglem7  21701  pzriprnglem13  21707  pzriprnglem14  21708  pzriprngALT  21709  preimaaa  26556  negleft  28324  negright  28325  oncutlt  28530  oniso  28537  n0fincut  28621  bdayn0sf1o  28636  dfnns2  28638  nohalf  28690  pw2recs  28704  z12negscl  28744  z12sge0  28749  remulscllem1  28766  remulscllem2  28767  tglnpt2  29001  plngrotlem1  29145  lnssplnglem  29149  lnssplng  29150  prlngd  29297  dfprlng2  29305  prlngex  29309  prlngmo2  29314  2exple2exp  33305  mndlrinvb  33466  mndlactfo  33468  mndractfo  33470  mndlactf1o  33471  mndractf1o  33472  gsumwrd2dccatlem  33518  elrgspnlem1  33683  elrgspnlem2  33684  elrgspnlem3  33685  elrgspnsubrunlem1  33688  elrgspnsubrunlem2  33689  rlocinvunit  33716  fracerl  33748  fracfld  33750  idomsubr  33751  dvdsruasso2  33820  mxidlirredi  33875  unitmulrprm  33939  1arithidomlem1  33946  1arithidom  33948  1arithufdlem1  33955  1arithufdlem2  33956  1arithufdlem3  33957  1arithufdlem4  33958  dfufd2lem  33960  zringfrac  33965  evl1deg1  33987  evl1deg2  33988  evl1deg3  33989  esplyfv1  34080  ply1degltdimlem  34133  fldextrspunlsp  34185  minplyelirng  34226  irredminply  34227  algextdeglem4  34231  algextdeglem8  34235  rtelextdg2lem  34237  fldext2chn  34239  constrmon  34255  constrextdg2lem  34259  constrextdg2  34260  ballotlem1c  35020  r1filimi  35612  vonf1oonfo  35713  nmulprop  36771  qdiff  38080  sn-negex12  43293  rediveud  43319  fsuppind  43437  prjspertr  43452  prjsperref  43453  prjspersym  43454  prjspvs  43457  0prjspnrel  43474  flt4lem2  43494  flt4lem7  43506  fourierdlem48  46983  fourierdlem49  46984  sqrtnnaa  47732  sqrtnzqaa  47733  isuspgrim0lem  48810  uhgrimisgrgriclem  48847  clnbgrgrim  48851  stgrnbgr0  48881  isubgr3stgrlem4  48886  uspgrlimlem2  48906  gpgedgvtx1  48979  gpgprismgr4cycllem3  49014  pgnbgreunbgr  49042  slotresfo  49826  exbaspos  49903  exbasprs  49904  oppff1o  50076  imaid  50081  diag1f1o  50461  diag2f1o  50464