Theorem rspceaimv 3612

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062

This theorem is referenced by:  brimralrspcev  5185  rexanre  15370  rexico  15377  rlim2lt  15518  rlim3  15519  rlimconst  15565  rlimcn3  15611  reccn2  15618  cn1lem  15619  o1rlimmul  15640  caucvgrlem  15694  divrcnv  15873  chfacffsupp  22799  chfacfscmulfsupp  22802  chfacfpmmulfsupp  22806  tsmsgsum  24082  tsmsres  24087  tsmsxp  24098  metcnpi3  24490  nrginvrcnlem  24635  nghmcn  24689  metdscn  24801  elcncf1di  24844  volcn  25564  itg2cnlem2  25720  abelthlem8  26406  divlogrlim  26601  cxplim  26939  cxploglim  26945  ftalem1  27040  ftalem2  27041  dchrisum0  27488  nmcvcn  30681  blocni  30791  0cnop  31965  0cnfn  31966  idcnop  31967  lnconi  32019  qqhcn  34027  dnicn  36515  ftc1anc  37730  limsupre3uzlem  45731  fourierdlem87  46189