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 343 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))) |
3 | 2 | ralbidv 3194 | . 2 ⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ 𝐶 (𝜑 → 𝜒) ↔ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒))) |
4 | 3 | rspcev 3620 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 (𝜑 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1528 ∈ wcel 2105 ∀wral 3135 ∃wrex 3136 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 df-clel 2890 df-ral 3140 df-rex 3141 |
This theorem is referenced by: brimralrspcev 5118 rexanre 14694 rexico 14701 rlim2lt 14842 rlim3 14843 rlimconst 14889 rlimcn2 14935 reccn2 14941 cn1lem 14942 o1rlimmul 14963 caucvgrlem 15017 divrcnv 15195 chfacffsupp 21392 chfacfscmulfsupp 21395 chfacfpmmulfsupp 21399 tsmsgsum 22674 tsmsres 22679 tsmsxp 22690 metcnpi3 23083 nrginvrcnlem 23227 nghmcn 23281 metdscn 23391 elcncf1di 23430 volcn 24134 itg2cnlem2 24290 abelthlem8 24954 divlogrlim 25145 cxplim 25476 cxploglim 25482 ftalem1 25577 ftalem2 25578 dchrisum0 26023 nmcvcn 28399 blocni 28509 0cnop 29683 0cnfn 29684 idcnop 29685 lnconi 29737 qqhcn 31131 dnicn 33728 ftc1anc 34856 limsupre3uzlem 41892 fourierdlem87 42355 |
Copyright terms: Public domain | W3C validator |