![]() |
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 345 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))) |
3 | 2 | ralbidv 3162 | . 2 ⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ 𝐶 (𝜑 → 𝜒) ↔ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒))) |
4 | 3 | rspcev 3571 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 (𝜑 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1538 ∈ wcel 2111 ∀wral 3106 ∃wrex 3107 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-cleq 2791 df-clel 2870 df-ral 3111 df-rex 3112 |
This theorem is referenced by: brimralrspcev 5091 rexanre 14698 rexico 14705 rlim2lt 14846 rlim3 14847 rlimconst 14893 rlimcn2 14939 reccn2 14945 cn1lem 14946 o1rlimmul 14967 caucvgrlem 15021 divrcnv 15199 chfacffsupp 21461 chfacfscmulfsupp 21464 chfacfpmmulfsupp 21468 tsmsgsum 22744 tsmsres 22749 tsmsxp 22760 metcnpi3 23153 nrginvrcnlem 23297 nghmcn 23351 metdscn 23461 elcncf1di 23500 volcn 24210 itg2cnlem2 24366 abelthlem8 25034 divlogrlim 25226 cxplim 25557 cxploglim 25563 ftalem1 25658 ftalem2 25659 dchrisum0 26104 nmcvcn 28478 blocni 28588 0cnop 29762 0cnfn 29763 idcnop 29764 lnconi 29816 qqhcn 31342 dnicn 33944 ftc1anc 35138 limsupre3uzlem 42377 fourierdlem87 42835 |
Copyright terms: Public domain | W3C validator |