Theorem rspcedvdw 3580

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088

This theorem is used by:  rspceb2dv  3581  prproe  4865  fnwe2lem3  8147  frxp2  8161  r1filimi  9903  elpq  13103  reltre  13471  rpltrp  13472  reltxrnmnf  13473  modmuladd  14056  modmuladdnn0  14058  ghmqusnsglem1  19494  opprring  20577  isdrng3lem1  21005  pzriprnglem7  21793  pzriprnglem13  21799  pzriprnglem14  21800  pzriprngALT  21801  preimaaa  26646  flt4lem2  27977  flt4lem7  27989  negleft  28444  negright  28445  oncutlt  28650  oniso  28657  n0fincut  28741  bdayn0sf1o  28756  dfnns2  28758  nohalf  28810  pw2recs  28824  z12negscl  28864  z12sge0  28869  remulscllem1  28886  remulscllem2  28887  tglnpt2  29121  plngrotlem1  29265  lnssplnglem  29269  lnssplng  29270  prlngd  29417  dfprlng2  29425  prlngex  29429  prlngmo2  29434  2exple2exp  33425  mndlrinvb  33586  mndlactfo  33588  mndractfo  33590  mndlactf1o  33591  mndractf1o  33592  gsumwrd2dccatlem  33638  elrgspnlem1  33803  elrgspnlem2  33804  elrgspnlem3  33805  elrgspnsubrunlem1  33808  elrgspnsubrunlem2  33809  rlocinvunit  33836  fracerl  33868  fracfld  33870  idomsubr  33871  dvdsruasso2  33941  mxidlirredi  33996  unitmulrprm  34060  1arithidomlem1  34067  1arithidom  34069  1arithufdlem1  34076  1arithufdlem2  34077  1arithufdlem3  34078  1arithufdlem4  34079  dfufd2lem  34081  zringfrac  34086  evl1deg1  34108  evl1deg2  34109  evl1deg3  34110  esplyfv1  34201  ply1degltdimlem  34254  fldextrspunlsp  34306  minplyelirng  34347  irredminply  34348  algextdeglem4  34352  algextdeglem8  34356  rtelextdg2lem  34358  fldext2chn  34360  constrmon  34376  constrextdg2lem  34380  constrextdg2  34381  ballotlem1c  35140  vonf1oonfo  35898  nmulprop  36939  qdiff  38248  sn-negex12  43468  rediveud  43494  fsuppind  43618  prjspertr  43633  prjsperref  43634  prjspersym  43635  prjspvs  43638  0prjspnrel  43663  fourierdlem48  47163  fourierdlem49  47164  sqrtnnaa  47912  sqrtnzqaa  47913  isuspgrim0lem  48990  uhgrimisgrgriclem  49027  clnbgrgrim  49031  stgrnbgr0  49061  isubgr3stgrlem4  49066  uspgrlimlem2  49086  gpgedgvtx1  49159  gpgprismgr4cycllem3  49194  pgnbgreunbgr  49222  slotresfo  50006  exbaspos  50083  exbasprs  50084  oppff1o  50256  imaid  50261  diag1f1o  50641  diag2f1o  50644