![]() |
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 334 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))) |
3 | 2 | ralbidv 3147 | . 2 ⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ 𝐶 (𝜑 → 𝜒) ↔ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒))) |
4 | 3 | rspcev 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 |