![]() |
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 2371. See nfrex 3371 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
Ref | Expression |
---|---|
nfralw.1 | ⊢ Ⅎ𝑥𝐴 |
nfralw.2 | ⊢ Ⅎ𝑥𝜑 |
Ref | Expression |
---|---|
nfrexw | ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nftru 1806 | . . 3 ⊢ Ⅎ𝑦⊤ | |
2 | nfralw.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐴) |
4 | nfralw.2 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
5 | 4 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝜑) |
6 | 1, 3, 5 | nfrexdw 3307 | . 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑) |
7 | 6 | mptru 1548 | 1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1542 Ⅎwnf 1785 Ⅎwnfc 2883 ∃wrex 3070 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-10 2137 ax-11 2154 ax-12 2171 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-nf 1786 df-clel 2810 df-nfc 2885 df-ral 3062 df-rex 3071 |
This theorem is referenced by: nfiun 5021 rexopabb 5522 nffr 5644 abrexex2g 7935 indexfi 9345 nfoi 9493 ixpiunwdom 9569 hsmexlem2 10406 iunfo 10518 iundom2g 10519 reclem2pr 11027 nfwrd 14477 nfsum1 15620 nfsum 15621 nfcprod1 15838 nfcprod 15839 ptclsg 23050 iunmbl2 25005 mbfsup 25112 limciun 25342 opreu2reuALT 31644 iundisjf 31749 xrofsup 31915 locfinreflem 32715 esum2d 32986 bnj873 33830 bnj1014 33867 bnj1123 33892 bnj1307 33929 bnj1445 33950 bnj1446 33951 bnj1467 33960 bnj1463 33961 poimirlem24 36380 poimirlem26 36382 poimirlem27 36383 indexa 36470 filbcmb 36477 sdclem2 36479 sdclem1 36480 fdc1 36483 sbcrexgOLD 41358 rexrabdioph 41367 rexfrabdioph 41368 elnn0rabdioph 41376 dvdsrabdioph 41383 oaun3lem1 41959 disjrnmpt2 43721 rnmptbdlem 43796 infrnmptle 43970 infxrunb3rnmpt 43975 climinff 44164 xlimmnfv 44387 xlimpnfv 44391 cncfshift 44427 stoweidlem53 44606 stoweidlem57 44610 fourierdlem48 44707 fourierdlem73 44732 sge0gerp 44948 sge0resplit 44959 sge0reuz 45000 meaiuninc3v 45037 smfsup 45367 smfsupmpt 45368 smfinf 45371 smfinfmpt 45372 cbvrex2 45648 2reu8i 45657 mogoldbb 46289 |
Copyright terms: Public domain | W3C validator |