Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rexlimiv | Structured version Visualization version GIF version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.) |
Ref | Expression |
---|---|
rexlimiv.1 | ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) |
Ref | Expression |
---|---|
rexlimiv | ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimiv.1 | . . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) | |
2 | 1 | rgen 2906 | . 2 ⊢ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) |
3 | r19.23v 3005 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)) | |
4 | 2, 3 | mpbi 219 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1977 ∀wral 2896 ∃wrex 2897 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-ral 2901 df-rex 2902 |
This theorem is referenced by: rexlimiva 3010 rexlimivw 3011 rexlimdv 3012 rexlimivv 3018 rexn0 4026 uniss2 4406 disjiun 4573 elres 5355 ssimaex 6173 ordzsl 6937 onzsl 6938 tfrlem8 7367 nneob 7619 ecoptocl 7724 mapsn 7785 elixpsn 7833 ixpsnf1o 7834 php 8029 php3 8031 ssfi 8065 findcard 8084 findcard2 8085 ordunifi 8095 fiint 8122 en3lp 8396 inf0 8401 inf3lemd 8407 inf3lem6 8413 noinfep 8440 cantnfvalf 8445 trcl 8487 bndrank 8587 rankc2 8617 tcrank 8630 ficardom 8670 ac10ct 8740 isinfcard 8798 alephfp 8814 dfac5lem4 8832 dfac2 8836 ackbij2 8948 fin23lem16 9040 fin23lem29 9046 fin17 9099 fin1a2lem6 9110 itunitc 9126 hsmexlem9 9130 axdc3lem2 9156 axdc3lem4 9158 axcclem 9162 zorn2lem7 9207 wunr1om 9420 tskr1om 9468 grothomex 9530 prnmadd 9698 ltaprlem 9745 mulgt0sr 9805 0re 9919 0cnALT 10149 renegcli 10221 peano2nn 10909 bndndx 11168 uzn0 11579 ublbneg 11649 om2uzrani 12613 uzrdgfni 12619 exprelprel 13126 rtrclreclem3 13648 rtrclind 13653 rexanuz2 13937 caurcvg 14255 caucvg 14257 infcvgaux1i 14428 vdwlem6 15528 dfgrp2e 17271 efgrelexlemb 17986 cygth 19739 iscldtop 20709 opnneiid 20740 pnfnei 20834 mnfnei 20835 discmp 21011 cmpsublem 21012 cmpfi 21021 2ndcredom 21063 2ndc1stc 21064 2ndcdisj 21069 kgenidm 21160 methaus 22135 xrtgioo 22417 caun0 22887 ovolmge0 23052 itg2lcl 23300 aannenlem2 23888 aannenlem3 23889 aaliou2 23899 leibpilem1 24467 2lgslem1b 24917 2sqlem2 24943 ostth 25128 eupatrl 26495 3cyclfrgrarn1 26539 3cyclfrgrarn 26540 h1de2ctlem 27798 h1de2ci 27799 spansni 27800 spanunsni 27822 riesz3i 28305 adjbd1o 28328 rnbra 28350 pjnmopi 28391 dfpjop 28425 atom1d 28596 cvexchlem 28611 cdj1i 28676 cdj3lem1 28677 hasheuni 29474 cvmlift2lem12 30550 mrsubccat 30669 msrid 30696 elmthm 30727 untint 30843 dfon2lem3 30934 dfon2lem7 30938 dfrdg2 30945 trpred0 30980 nodmon 31047 sltval2 31053 bdayfo 31074 nofulllem5 31105 finminlem 31482 fneint 31513 ptrecube 32579 poimirlem26 32605 poimirlem27 32606 poimirlem29 32608 poimirlem30 32609 zerdivemp1x 32916 dochsnnz 35757 ismrc 36282 eldiophb 36338 eldioph4b 36393 dfacbasgrp 36697 subsaliuncllem 39251 icoresmbl 39433 prmdvdsfmtnof1lem2 40035 clel5 40303 3cyclfrgrrn1 41455 3cyclfrgrrn 41456 |
Copyright terms: Public domain | W3C validator |