Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspceaimv Structured version   Visualization version   GIF version

Theorem rspceaimv 3543
 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
StepHypRef Expression
1 rspceaimv.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
21imbi1d 334 . . 3 (𝑥 = 𝐴 → ((𝜑𝜒) ↔ (𝜓𝜒)))
32ralbidv 3147 . 2 (𝑥 = 𝐴 → (∀𝑦𝐶 (𝜑𝜒) ↔ ∀𝑦𝐶 (𝜓𝜒)))
43rspcev 3535 1 ((𝐴𝐵 ∧ ∀𝑦𝐶 (𝜓𝜒)) → ∃𝑥𝐵𝑦𝐶 (𝜑𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1507   ∈ wcel 2050  ∀wral 3088  ∃wrex 3089 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-v 3417 This theorem is referenced by:  brimralrspcev  4991  rexanre  14570  rexico  14577  rlim2lt  14718  rlim3  14719  rlimconst  14765  rlimcn2  14811  reccn2  14817  cn1lem  14818  o1rlimmul  14839  caucvgrlem  14893  divrcnv  15070  chfacffsupp  21171  chfacfscmulfsupp  21174  chfacfpmmulfsupp  21178  tsmsgsum  22453  tsmsres  22458  tsmsxp  22469  metcnpi3  22862  nrginvrcnlem  23006  nghmcn  23060  metdscn  23170  elcncf1di  23209  volcn  23913  itg2cnlem2  24069  abelthlem8  24733  divlogrlim  24922  cxplim  25254  cxploglim  25260  ftalem1  25355  ftalem2  25356  dchrisum0  25801  nmcvcn  28252  blocni  28362  0cnop  29540  0cnfn  29541  idcnop  29542  lnconi  29594  qqhcn  30876  dnicn  33351  ftc1anc  34416  limsupre3uzlem  41448  fourierdlem87  41910
 Copyright terms: Public domain W3C validator