![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rspe | Structured version Visualization version GIF version |
Description: Restricted specialization. (Contributed by NM, 12-Oct-1999.) |
Ref | Expression |
---|---|
rspe | ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.8a 2109 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | df-rex 3088 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
3 | 1, 2 | sylibr 226 | 1 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∃wex 1742 ∈ wcel 2050 ∃wrex 3083 |
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-12 2106 |
This theorem depends on definitions: df-bi 199 df-ex 1743 df-rex 3088 |
This theorem is referenced by: rsp2e 3244 2rmorex 3648 2reurex 3653 ssiun2 4831 reusv2lem3 5148 tfrlem9 7819 isinf 8520 findcard2 8547 findcard3 8550 scott0 9103 ac6c4 9695 supaddc 11403 supadd 11404 supmul1 11405 supmul 11408 fsuppmapnn0fiub 13168 mreiincl 16719 restmetu 22877 bposlem3 25558 opphllem5 26233 pjpjpre 28971 atom1d 29905 actfunsnf1o 31523 bnj1398 31951 cvmlift2lem12 32146 nosupbnd1 32735 nosupbnd2 32737 finminlem 33187 neibastop2lem 33229 iooelexlt 34085 relowlpssretop 34087 ralssiun 34129 prtlem18 35458 pell14qrdich 38862 eliuniin 40787 eliuniin2 40809 eliunid 40841 disjinfi 40878 iunmapsn 40905 fvelimad 40945 infnsuprnmpt 40950 upbdrech 41001 limclner 41363 limsupre3uzlem 41447 climuzlem 41455 sge0iunmptlemre 42128 iundjiun 42173 meaiininclem 42199 isomenndlem 42243 ovnsubaddlem1 42283 vonioo 42395 vonicc 42398 smfaddlem1 42470 f1oresf1o2 42896 |
Copyright terms: Public domain | W3C validator |