Theorem rspceaimv 3588

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 3188	. 2 ⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ 𝐶 (𝜑 → 𝜒) ↔ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒)))
4	3	rspcev 3582	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 (𝜑 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∀wral 3079  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090

This theorem is referenced by:  brimralrspcev  5173  rexanre  15400  rexico  15407  rlim2lt  15550  rlim3  15551  rlimconst  15597  rlimcn3  15643  reccn2  15650  cn1lem  15651  o1rlimmul  15672  caucvgrlem  15726  divrcnv  15908  chfacffsupp  22994  chfacfscmulfsupp  22997  chfacfpmmulfsupp  23001  tsmsgsum  24277  tsmsres  24282  tsmsxp  24293  metcnpi3  24684  nrginvrcnlem  24829  nghmcn  24883  metdscn  24995  elcncf1di  25035  volcn  25746  itg2cnlem2  25902  abelthlem8  26583  divlogrlim  26781  cxplim  27117  cxploglim  27123  ftalem1  27218  ftalem2  27219  dchrisum0  27665  nmcvcn  31028  blocni  31138  0cnop  32312  0cnfn  32313  idcnop  32314  lnconi  32366  qqhcn  34362  dnicn  37062  ftc1anc  38333  limsupre3uzlem  46432  fourierdlem87  46890