Theorem rspceaimv 3582

Description: Restricted existential specialization of a universally quantified implication. (Contributed by BJ, 24-Aug-2022.)

Hypothesis

Ref	Expression
rspceaimv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rspceaimv	⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 (𝜑 → 𝜒))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵   𝑥,𝐶   𝜓,𝑥   𝜒,𝑥

Allowed substitution hints:   𝜑(𝑥, 𝑦)   𝜓(𝑦)   𝜒(𝑦)   𝐵(𝑦)   𝐶(𝑦)

Proof of Theorem rspceaimv

Step	Hyp	Ref	Expression
1		rspceaimv.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	imbi1d 344	. . 3 ⊢ (𝑥 = 𝐴 → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)))
3	2	ralbidv 3185	. 2 ⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ 𝐶 (𝜑 → 𝜒) ↔ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒)))
4	3	rspcev 3576	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 (𝜑 → 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∀wral 3076  ∃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:  brimralrspcev  5165  rexanre  15520  rexico  15527  rlim2lt  15670  rlim3  15671  rlimconst  15717  rlimcn3  15763  reccn2  15770  cn1lem  15771  o1rlimmul  15792  caucvgrlem  15846  divrcnv  16027  chfacffsupp  23180  chfacfscmulfsupp  23183  chfacfpmmulfsupp  23187  tsmsgsum  24464  tsmsres  24469  tsmsxp  24480  metcnpi3  24871  nrginvrcnlem  25016  nghmcn  25070  metdscn  25182  elcncf1di  25222  volcn  25933  itg2cnlem2  26089  abelthlem8  26772  divlogrlim  26969  cxplim  27305  cxploglim  27311  ftalem1  27406  ftalem2  27407  dchrisum0  27853  nmcvcn  31303  blocni  31413  0cnop  32587  0cnfn  32588  idcnop  32589  lnconi  32641  qqhcn  34670  dnicn  37451  ftc1anc  38713  limsupre3uzlem  46839  fourierdlem87  47297