![]() |
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 341 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))) |
3 | 2 | ralbidv 3176 | . 2 ⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ 𝐶 (𝜑 → 𝜒) ↔ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒))) |
4 | 3 | rspcev 3622 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 (𝜑 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1537 ∈ wcel 2106 ∀wral 3059 ∃wrex 3068 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-ral 3060 df-rex 3069 |
This theorem is referenced by: brimralrspcev 5209 rexanre 15382 rexico 15389 rlim2lt 15530 rlim3 15531 rlimconst 15577 rlimcn3 15623 reccn2 15630 cn1lem 15631 o1rlimmul 15652 caucvgrlem 15706 divrcnv 15885 chfacffsupp 22878 chfacfscmulfsupp 22881 chfacfpmmulfsupp 22885 tsmsgsum 24163 tsmsres 24168 tsmsxp 24179 metcnpi3 24575 nrginvrcnlem 24728 nghmcn 24782 metdscn 24892 elcncf1di 24935 volcn 25655 itg2cnlem2 25812 abelthlem8 26498 divlogrlim 26692 cxplim 27030 cxploglim 27036 ftalem1 27131 ftalem2 27132 dchrisum0 27579 nmcvcn 30724 blocni 30834 0cnop 32008 0cnfn 32009 idcnop 32010 lnconi 32062 qqhcn 33954 dnicn 36475 ftc1anc 37688 limsupre3uzlem 45691 fourierdlem87 46149 |
Copyright terms: Public domain | W3C validator |