Theorem rspcedvdw 3638

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077

This theorem is referenced by:  prproe  4929  frxp2  8185  elpq  13040  reltre  13402  rpltrp  13403  reltxrnmnf  13404  modmuladd  13964  modmuladdnn0  13966  ghmqusnsglem1  19320  opprring  20373  pzriprnglem7  21521  pzriprnglem13  21527  pzriprnglem14  21528  pzriprngALT  21529  dfnns2  28380  remulscllem1  28450  remulscllem2  28451  mndlrinvb  33011  mndlactfo  33013  mndractfo  33015  mndlactf1o  33016  mndractf1o  33017  fracerl  33273  fracfld  33275  idomsubr  33276  dvdsruasso2  33379  unitmulrprm  33521  1arithidomlem1  33528  1arithidom  33530  1arithufdlem1  33537  1arithufdlem2  33538  1arithufdlem3  33539  1arithufdlem4  33540  dfufd2lem  33542  zringfrac  33547  evl1deg1  33566  evl1deg2  33567  evl1deg3  33568  ply1degltdimlem  33635  irredminply  33707  algextdeglem4  33711  algextdeglem8  33715  rtelextdg2lem  33717  fldext2chn  33719  constrmon  33734  sn-negex12  42392  fsuppind  42545  prjspertr  42560  prjsperref  42561  prjspersym  42562  prjspvs  42565  0prjspnrel  42582  flt4lem2  42602  flt4lem7  42614  isuspgrim0lem  47755  uhgrimisgrgriclem  47782  clnbgrgrim  47786  uspgrlimlem2  47813