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 2922 | . 2 ⊢ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) |
3 | r19.23v 3023 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)) | |
4 | 2, 3 | mpbi 220 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1990 ∀wral 2912 ∃wrex 2913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-ral 2917 df-rex 2918 |
This theorem is referenced by: rexlimiva 3028 rexlimivw 3029 rexlimdv 3030 rexlimivv 3036 clel5 3343 rexn0 4074 issn 4363 uniss2 4470 disjiun 4640 elres 5435 ssimaex 6263 ordzsl 7045 onzsl 7046 tfrlem8 7480 nneob 7732 ecoptocl 7837 mapsn 7899 elixpsn 7947 ixpsnf1o 7948 php 8144 php3 8146 ssfi 8180 findcard 8199 findcard2 8200 ordunifi 8210 fiint 8237 en3lp 8513 inf0 8518 inf3lemd 8524 inf3lem6 8530 noinfep 8557 cantnfvalf 8562 trcl 8604 bndrank 8704 rankc2 8734 tcrank 8747 ficardom 8787 ac10ct 8857 isinfcard 8915 alephfp 8931 dfac5lem4 8949 dfac2 8953 ackbij2 9065 fin23lem16 9157 fin23lem29 9163 fin17 9216 fin1a2lem6 9227 itunitc 9243 hsmexlem9 9247 axdc3lem2 9273 axdc3lem4 9275 axcclem 9279 zorn2lem7 9324 wunr1om 9541 tskr1om 9589 grothomex 9651 prnmadd 9819 ltaprlem 9866 mulgt0sr 9926 0re 10040 0cnALT 10270 renegcli 10342 peano2nn 11032 bndndx 11291 uzn0 11703 ublbneg 11773 om2uzrani 12751 uzrdgfni 12757 exprelprel 13271 rtrclreclem3 13800 rtrclind 13805 rexanuz2 14089 caurcvg 14407 caucvg 14409 infcvgaux1i 14589 vdwlem6 15690 dfgrp2e 17448 efgrelexlemb 18163 cygth 19920 iscldtop 20899 opnneiid 20930 pnfnei 21024 mnfnei 21025 discmp 21201 cmpsublem 21202 cmpfi 21211 2ndcredom 21253 2ndc1stc 21254 2ndcdisj 21259 kgenidm 21350 methaus 22325 xrtgioo 22609 caun0 23079 ovolmge0 23245 itg2lcl 23494 aannenlem2 24084 aannenlem3 24085 aaliou2 24095 leibpilem1 24667 2lgslem1b 25117 2sqlem2 25143 ostth 25328 midwwlks2s3 26860 3cyclfrgrrn1 27149 3cyclfrgrrn 27150 h1de2ctlem 28414 h1de2ci 28415 spansni 28416 spanunsni 28438 riesz3i 28921 adjbd1o 28944 rnbra 28966 pjnmopi 29007 dfpjop 29041 atom1d 29212 cvexchlem 29227 cdj1i 29292 cdj3lem1 29293 hasheuni 30147 cvmlift2lem12 31296 mrsubccat 31415 msrid 31442 elmthm 31473 untint 31589 dfon2lem3 31690 dfon2lem7 31694 dfrdg2 31701 trpred0 31736 nodmon 31803 sltval2 31809 bdayfo 31828 finminlem 32312 fneint 32343 ptrecube 33409 poimirlem26 33435 poimirlem27 33436 poimirlem29 33438 poimirlem30 33439 zerdivemp1x 33746 dochsnnz 36739 ismrc 37264 eldiophb 37320 eldioph4b 37375 dfacbasgrp 37678 subsaliuncllem 40575 icoresmbl 40757 prmdvdsfmtnof1lem2 41497 sprsymrelfvlem 41740 sprsymrelf1lem 41741 uspgropssxp 41752 |
Copyright terms: Public domain | W3C validator |