Theorem rspceaimv 3594

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054

This theorem is referenced by:  brimralrspcev  5168  rexanre  15313  rexico  15320  rlim2lt  15463  rlim3  15464  rlimconst  15510  rlimcn3  15556  reccn2  15563  cn1lem  15564  o1rlimmul  15585  caucvgrlem  15639  divrcnv  15818  chfacffsupp  22743  chfacfscmulfsupp  22746  chfacfpmmulfsupp  22750  tsmsgsum  24026  tsmsres  24031  tsmsxp  24042  metcnpi3  24434  nrginvrcnlem  24579  nghmcn  24633  metdscn  24745  elcncf1di  24788  volcn  25507  itg2cnlem2  25663  abelthlem8  26349  divlogrlim  26544  cxplim  26882  cxploglim  26888  ftalem1  26983  ftalem2  26984  dchrisum0  27431  nmcvcn  30624  blocni  30734  0cnop  31908  0cnfn  31909  idcnop  31910  lnconi  31962  qqhcn  33981  dnicn  36480  ftc1anc  37695  limsupre3uzlem  45733  fourierdlem87  46191