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 344 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))) |
3 | 2 | ralbidv 3197 | . 2 ⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ 𝐶 (𝜑 → 𝜒) ↔ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒))) |
4 | 3 | rspcev 3623 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 (𝜑 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1537 ∈ wcel 2114 ∀wral 3138 ∃wrex 3139 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-cleq 2814 df-clel 2893 df-ral 3143 df-rex 3144 |
This theorem is referenced by: brimralrspcev 5127 rexanre 14706 rexico 14713 rlim2lt 14854 rlim3 14855 rlimconst 14901 rlimcn2 14947 reccn2 14953 cn1lem 14954 o1rlimmul 14975 caucvgrlem 15029 divrcnv 15207 chfacffsupp 21464 chfacfscmulfsupp 21467 chfacfpmmulfsupp 21471 tsmsgsum 22747 tsmsres 22752 tsmsxp 22763 metcnpi3 23156 nrginvrcnlem 23300 nghmcn 23354 metdscn 23464 elcncf1di 23503 volcn 24207 itg2cnlem2 24363 abelthlem8 25027 divlogrlim 25218 cxplim 25549 cxploglim 25555 ftalem1 25650 ftalem2 25651 dchrisum0 26096 nmcvcn 28472 blocni 28582 0cnop 29756 0cnfn 29757 idcnop 29758 lnconi 29810 qqhcn 31232 dnicn 33831 ftc1anc 34990 limsupre3uzlem 42065 fourierdlem87 42527 |
Copyright terms: Public domain | W3C validator |