| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > nfrexw | Structured version Visualization version GIF version | ||
| Description: Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2019.) Add disjoint variable condition to avoid ax-13 2377. See nfrex 3375 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.) |
| Ref | Expression |
|---|---|
| nfralw.1 | ⊢ Ⅎ𝑥𝐴 |
| nfralw.2 | ⊢ Ⅎ𝑥𝜑 |
| Ref | Expression |
|---|---|
| nfrexw | ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nftru 1804 | . . 3 ⊢ Ⅎ𝑦⊤ | |
| 2 | nfralw.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
| 3 | 2 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐴) |
| 4 | nfralw.2 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
| 5 | 4 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝜑) |
| 6 | 1, 3, 5 | nfrexdw 3310 | . 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑) |
| 7 | 6 | mptru 1547 | 1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: ⊤wtru 1541 Ⅎwnf 1783 Ⅎwnfc 2890 ∃wrex 3070 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-10 2141 ax-11 2157 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-clel 2816 df-nfc 2892 df-ral 3062 df-rex 3071 |
| This theorem is referenced by: nfiun 5023 rexopabb 5533 nffr 5658 abrexex2g 7989 indexfi 9400 nfoi 9554 ixpiunwdom 9630 hsmexlem2 10467 iunfo 10579 iundom2g 10580 reclem2pr 11088 nfwrd 14581 nfsum1 15726 nfsum 15727 nfcprod1 15944 nfcprod 15945 ptclsg 23623 iunmbl2 25592 mbfsup 25699 limciun 25929 opreu2reuALT 32496 iundisjf 32602 xrofsup 32771 locfinreflem 33839 esum2d 34094 bnj873 34938 bnj1014 34975 bnj1123 35000 bnj1307 35037 bnj1445 35058 bnj1446 35059 bnj1467 35068 bnj1463 35069 poimirlem24 37651 poimirlem26 37653 poimirlem27 37654 indexa 37740 filbcmb 37747 sdclem2 37749 sdclem1 37750 fdc1 37753 sbcrexgOLD 42796 rexrabdioph 42805 rexfrabdioph 42806 elnn0rabdioph 42814 dvdsrabdioph 42821 oaun3lem1 43387 modelaxreplem3 44997 modelaxrep 44998 disjrnmpt2 45193 rnmptbdlem 45262 infrnmptle 45434 infxrunb3rnmpt 45439 climinff 45626 xlimmnfv 45849 xlimpnfv 45853 cncfshift 45889 stoweidlem53 46068 stoweidlem57 46072 fourierdlem48 46169 fourierdlem73 46194 sge0gerp 46410 sge0resplit 46421 sge0reuz 46462 meaiuninc3v 46499 smfsup 46829 smfsupmpt 46830 smfinf 46833 smfinfmpt 46834 cbvrex2 47116 2reu8i 47125 mogoldbb 47772 |
| Copyright terms: Public domain | W3C validator |