Theorem rspcedvdw 3583

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091

This theorem is used by:  rspceb2dv  3584  rspc2ev  3592  prproe  4838  fnwe2lem3  8184  frxp2  8198  r1filimi  9940  elpq  13143  reltre  13511  rpltrp  13512  reltxrnmnf  13513  modmuladd  14096  modmuladdnn0  14098  ghmqusnsglem1  19545  opprring  20628  isdrng3lem1  21056  pzriprnglem7  21848  pzriprnglem13  21854  pzriprnglem14  21855  pzriprngALT  21856  preimaaa  26703  qaa  26704  flt4lem2  28034  flt4lem7  28046  negleft  28501  negright  28502  oncutlt  28707  oniso  28714  n0fincut  28798  bdayn0sf1o  28813  dfnns2  28815  nohalf  28867  pw2recs  28881  z12negscl  28921  z12sge0  28926  remulscllem1  28943  remulscllem2  28944  tglnpt2  29178  plngrotlem1  29322  lnssplnglem  29326  lnssplng  29327  prlngd  29474  dfprlng2  29482  prlngex  29486  prlngmo2  29491  foresf1o  33199  2exple2exp  33521  weinfcl  33636  weinflb  33637  mndlrinvb  33685  mndlactfo  33687  mndractfo  33689  mndlactf1o  33690  mndractf1o  33691  gsumwrd2dccatlem  33737  elrgspnlem1  33902  elrgspnlem2  33903  elrgspnlem3  33904  elrgspnsubrunlem1  33907  elrgspnsubrunlem2  33908  rlocinvunit  33935  edompid  33961  fracerl  33972  fracfld  33974  idomsubr  33975  dvdsruasso2  34045  elrspunidl  34082  mxidlirredi  34100  unitmulrprm  34164  1arithidomlem1  34171  1arithidom  34173  1arithufdlem1  34180  1arithufdlem2  34181  1arithufdlem3  34182  1arithufdlem4  34183  dfufd2lem  34185  zringfrac  34189  evl1deg1  34211  evl1deg2  34212  evl1deg3  34213  esplyfv1  34312  ply1degltdimlem  34365  fldextrspunlsp  34417  minplyelirng  34458  irredminply  34459  algextdeglem4  34463  algextdeglem8  34467  rtelextdg2lem  34469  fldext2chn  34471  constrmon  34487  constrextdg2lem  34491  constrextdg2  34492  reff  34582  cmpcref  34593  ballotlem1c  35251  dfac16  35887  vonf1oonfo  36090  nmulprop  37154  qdiff  38516  sn-negex12  43734  rediveud  43760  fsuppind  43884  prjspertr  43899  prjsperref  43900  prjspersym  43901  prjspvs  43904  0prjspnrel  43929  fingrphf  46300  fourierdlem48  47437  fourierdlem49  47438  sqrtnnaa  48186  sqrtnzqaa  48187  isuspgrim0lem  49264  uhgrimisgrgriclem  49301  clnbgrgrim  49305  stgrnbgr0  49335  isubgr3stgrlem4  49340  uspgrlimlem2  49360  gpgedgvtx1  49433  gpgprismgr4cycllem3  49468  pgnbgreunbgr  49496  line2ylem  50194  line2xlem  50196  slotresfo  50344  exbaspos  50421  exbasprs  50422  oppff1o  50596  imaid  50601  diag1f1o  51000  diag2f1o  51006