Theorem rspcedvdw 3625

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2106  ∃wrex 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069

This theorem is referenced by:  prproe  4910  frxp2  8168  elpq  13015  reltre  13379  rpltrp  13380  reltxrnmnf  13381  modmuladd  13951  modmuladdnn0  13953  ghmqusnsglem1  19311  opprring  20364  pzriprnglem7  21516  pzriprnglem13  21522  pzriprnglem14  21523  pzriprngALT  21524  dfnns2  28377  remulscllem1  28447  remulscllem2  28448  mndlrinvb  33013  mndlactfo  33015  mndractfo  33017  mndlactf1o  33018  mndractf1o  33019  gsumwrd2dccatlem  33052  elrgspnlem1  33232  elrgspnlem2  33233  elrgspnlem3  33234  fracerl  33288  fracfld  33290  idomsubr  33291  dvdsruasso2  33394  unitmulrprm  33536  1arithidomlem1  33543  1arithidom  33545  1arithufdlem1  33552  1arithufdlem2  33553  1arithufdlem3  33554  1arithufdlem4  33555  dfufd2lem  33557  zringfrac  33562  evl1deg1  33581  evl1deg2  33582  evl1deg3  33583  ply1degltdimlem  33650  irredminply  33722  algextdeglem4  33726  algextdeglem8  33730  rtelextdg2lem  33732  fldext2chn  33734  constrmon  33749  sn-negex12  42423  fsuppind  42577  prjspertr  42592  prjsperref  42593  prjspersym  42594  prjspvs  42597  0prjspnrel  42614  flt4lem2  42634  flt4lem7  42646  isuspgrim0lem  47809  uhgrimisgrgriclem  47836  clnbgrgrim  47840  stgrnbgr0  47867  isubgr3stgrlem4  47872  uspgrlimlem2  47892  gpgedgvtx1  47955