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 3120 | . 2 ⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ 𝐶 (𝜑 → 𝜒) ↔ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒))) |
4 | 3 | rspcev 3552 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 (𝜑 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1539 ∈ wcel 2108 ∀wral 3063 ∃wrex 3064 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1542 df-ex 1784 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2817 df-ral 3068 df-rex 3069 |
This theorem is referenced by: brimralrspcev 5131 rexanre 14986 rexico 14993 rlim2lt 15134 rlim3 15135 rlimconst 15181 rlimcn3 15227 reccn2 15234 cn1lem 15235 o1rlimmul 15256 caucvgrlem 15312 divrcnv 15492 chfacffsupp 21913 chfacfscmulfsupp 21916 chfacfpmmulfsupp 21920 tsmsgsum 23198 tsmsres 23203 tsmsxp 23214 metcnpi3 23608 nrginvrcnlem 23761 nghmcn 23815 metdscn 23925 elcncf1di 23964 volcn 24675 itg2cnlem2 24832 abelthlem8 25503 divlogrlim 25695 cxplim 26026 cxploglim 26032 ftalem1 26127 ftalem2 26128 dchrisum0 26573 nmcvcn 28958 blocni 29068 0cnop 30242 0cnfn 30243 idcnop 30244 lnconi 30296 qqhcn 31841 dnicn 34599 ftc1anc 35785 limsupre3uzlem 43166 fourierdlem87 43624 |
Copyright terms: Public domain | W3C validator |