|   | 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 3177 | . 2 ⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ 𝐶 (𝜑 → 𝜒) ↔ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒))) | 
| 4 | 3 | rspcev 3621 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 (𝜑 → 𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1539 ∈ wcel 2107 ∀wral 3060 ∃wrex 3069 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-ral 3061 df-rex 3070 | 
| This theorem is referenced by: brimralrspcev 5203 rexanre 15386 rexico 15393 rlim2lt 15534 rlim3 15535 rlimconst 15581 rlimcn3 15627 reccn2 15634 cn1lem 15635 o1rlimmul 15656 caucvgrlem 15710 divrcnv 15889 chfacffsupp 22863 chfacfscmulfsupp 22866 chfacfpmmulfsupp 22870 tsmsgsum 24148 tsmsres 24153 tsmsxp 24164 metcnpi3 24560 nrginvrcnlem 24713 nghmcn 24767 metdscn 24879 elcncf1di 24922 volcn 25642 itg2cnlem2 25798 abelthlem8 26484 divlogrlim 26678 cxplim 27016 cxploglim 27022 ftalem1 27117 ftalem2 27118 dchrisum0 27565 nmcvcn 30715 blocni 30825 0cnop 31999 0cnfn 32000 idcnop 32001 lnconi 32053 qqhcn 33993 dnicn 36494 ftc1anc 37709 limsupre3uzlem 45755 fourierdlem87 46213 | 
| Copyright terms: Public domain | W3C validator |