Theorem rspceaimv 3566

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1542   ∈ wcel 2110  ∀wral 3066  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-ral 3071  df-rex 3072

This theorem is referenced by:  brimralrspcev  5140  rexanre  15056  rexico  15063  rlim2lt  15204  rlim3  15205  rlimconst  15251  rlimcn3  15297  reccn2  15304  cn1lem  15305  o1rlimmul  15326  caucvgrlem  15382  divrcnv  15562  chfacffsupp  22003  chfacfscmulfsupp  22006  chfacfpmmulfsupp  22010  tsmsgsum  23288  tsmsres  23293  tsmsxp  23304  metcnpi3  23700  nrginvrcnlem  23853  nghmcn  23907  metdscn  24017  elcncf1di  24056  volcn  24768  itg2cnlem2  24925  abelthlem8  25596  divlogrlim  25788  cxplim  26119  cxploglim  26125  ftalem1  26220  ftalem2  26221  dchrisum0  26666  nmcvcn  29053  blocni  29163  0cnop  30337  0cnfn  30338  idcnop  30339  lnconi  30391  qqhcn  31937  dnicn  34668  ftc1anc  35854  limsupre3uzlem  43247  fourierdlem87  43705