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 1569   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

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

This theorem is used by:  rspceb2dv  3580  rspc2ev  3588  prproe  4832  fnwe2lem3  8154  frxp2  8168  r1filimi  9910  elpq  13110  reltre  13478  rpltrp  13479  reltxrnmnf  13480  modmuladd  14063  modmuladdnn0  14065  ghmqusnsglem1  19503  opprring  20586  isdrng3lem1  21014  pzriprnglem7  21802  pzriprnglem13  21808  pzriprnglem14  21809  pzriprngALT  21810  preimaaa  26655  qaa  26656  flt4lem2  27986  flt4lem7  27998  negleft  28453  negright  28454  oncutlt  28659  oniso  28666  n0fincut  28750  bdayn0sf1o  28765  dfnns2  28767  nohalf  28819  pw2recs  28833  z12negscl  28873  z12sge0  28878  remulscllem1  28895  remulscllem2  28896  tglnpt2  29130  plngrotlem1  29274  lnssplnglem  29278  lnssplng  29279  prlngd  29426  dfprlng2  29434  prlngex  29438  prlngmo2  29443  foresf1o  33151  2exple2exp  33475  mndlrinvb  33636  mndlactfo  33638  mndractfo  33640  mndlactf1o  33641  mndractf1o  33642  gsumwrd2dccatlem  33688  elrgspnlem1  33853  elrgspnlem2  33854  elrgspnlem3  33855  elrgspnsubrunlem1  33858  elrgspnsubrunlem2  33859  rlocinvunit  33886  fracerl  33918  fracfld  33920  idomsubr  33921  dvdsruasso2  33991  elrspunidl  34028  mxidlirredi  34046  unitmulrprm  34110  1arithidomlem1  34117  1arithidom  34119  1arithufdlem1  34126  1arithufdlem2  34127  1arithufdlem3  34128  1arithufdlem4  34129  dfufd2lem  34131  zringfrac  34136  evl1deg1  34158  evl1deg2  34159  evl1deg3  34160  esplyfv1  34251  ply1degltdimlem  34304  fldextrspunlsp  34356  minplyelirng  34397  irredminply  34398  algextdeglem4  34402  algextdeglem8  34406  rtelextdg2lem  34408  fldext2chn  34410  constrmon  34426  constrextdg2lem  34430  constrextdg2  34431  reff  34521  cmpcref  34532  ballotlem1c  35190  dfac16  35822  vonf1oonfo  36000  nmulprop  37063  qdiff  38385  sn-negex12  43605  rediveud  43631  fsuppind  43755  prjspertr  43770  prjsperref  43771  prjspersym  43772  prjspvs  43775  0prjspnrel  43800  fourierdlem48  47300  fourierdlem49  47301  sqrtnnaa  48049  sqrtnzqaa  48050  isuspgrim0lem  49127  uhgrimisgrgriclem  49164  clnbgrgrim  49168  stgrnbgr0  49198  isubgr3stgrlem4  49203  uspgrlimlem2  49223  gpgedgvtx1  49296  gpgprismgr4cycllem3  49331  pgnbgreunbgr  49359  line2ylem  49999  line2xlem  50001  slotresfo  50149  exbaspos  50226  exbasprs  50227  oppff1o  50401  imaid  50406  diag1f1o  50805  diag2f1o  50811