![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rspceaimv | Structured version Visualization version GIF version |
Description: Restricted existential specialization of a universally quantified implication. (Contributed by BJ, 24-Aug-2022.) |
Ref | Expression |
---|---|
rspceaimv.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
rspceaimv | ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 (𝜑 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspceaimv.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
2 | 1 | imbi1d 340 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))) |
3 | 2 | ralbidv 3167 | . 2 ⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ 𝐶 (𝜑 → 𝜒) ↔ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒))) |
4 | 3 | rspcev 3606 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 (𝜑 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1533 ∈ wcel 2098 ∀wral 3050 ∃wrex 3059 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-rex 3060 |
This theorem is referenced by: brimralrspcev 5210 rexanre 15329 rexico 15336 rlim2lt 15477 rlim3 15478 rlimconst 15524 rlimcn3 15570 reccn2 15577 cn1lem 15578 o1rlimmul 15599 caucvgrlem 15655 divrcnv 15834 chfacffsupp 22802 chfacfscmulfsupp 22805 chfacfpmmulfsupp 22809 tsmsgsum 24087 tsmsres 24092 tsmsxp 24103 metcnpi3 24499 nrginvrcnlem 24652 nghmcn 24706 metdscn 24816 elcncf1di 24859 volcn 25579 itg2cnlem2 25736 abelthlem8 26421 divlogrlim 26614 cxplim 26949 cxploglim 26955 ftalem1 27050 ftalem2 27051 dchrisum0 27498 nmcvcn 30577 blocni 30687 0cnop 31861 0cnfn 31862 idcnop 31863 lnconi 31915 qqhcn 33720 dnicn 36095 ftc1anc 37302 limsupre3uzlem 45258 fourierdlem87 45716 |
Copyright terms: Public domain | W3C validator |