Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfral | 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.) |
Ref | Expression |
---|---|
nfral.1 | ⊢ Ⅎ𝑥𝐴 |
nfral.2 | ⊢ Ⅎ𝑥𝜑 |
Ref | Expression |
---|---|
nfral | ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nftru 1721 | . . 3 ⊢ Ⅎ𝑦⊤ | |
2 | nfral.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐴) |
4 | nfral.2 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
5 | 4 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝜑) |
6 | 1, 3, 5 | nfrald 2928 | . 2 ⊢ (⊤ → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑) |
7 | 6 | trud 1484 | 1 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1476 Ⅎwnf 1699 Ⅎwnfc 2738 ∀wral 2896 |
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 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 |
This theorem is referenced by: nfra2 2930 rspc2 3292 sbcralt 3477 raaan 4032 nfint 4421 nfiin 4485 disjxun 4581 nfpo 4964 nfso 4965 nffr 5012 nfse 5013 ralxpf 5190 wfisg 5632 dff13f 6417 nfiso 6472 mpt2eq123 6612 fun11iun 7019 fmpt2x 7125 ovmptss 7145 nfwrecs 7296 xpf1o 8007 ac6sfi 8089 nfoi 8302 scottexs 8633 scott0s 8634 lble 10854 nnwof 11630 fzrevral 12294 rlimcld2 14157 fsum2dlem 14343 fsumcom2 14347 fsumcom2OLD 14348 fprod2dlem 14549 fprodcom2 14553 fprodcom2OLD 14554 gsummoncoe1 19495 cnmpt21 21284 cfilucfil 22174 ulmss 23955 fsumdvdscom 24711 dchrisumlema 24977 dchrisumlem2 24979 cnlnadjlem5 28314 disjabrex 28777 disjabrexf 28778 aciunf1lem 28844 ordtconlem1 29298 esumiun 29483 bnj1366 30154 bnj1385 30157 bnj981 30274 bnj1228 30333 bnj1398 30356 bnj1445 30366 bnj1449 30370 bnj1463 30377 untsucf 30841 setinds 30927 tfisg 30960 frinsg 30986 poimirlem26 32605 poimirlem27 32606 indexdom 32699 filbcmb 32705 sdclem1 32709 scottexf 33146 scott0f 33147 cdleme31sn1 34687 cdlemk36 35219 setindtrs 36610 evth2f 38197 evthf 38209 uzwo4 38246 eliuniincex 38323 disjinfi 38375 choicefi 38387 ssfiunibd 38464 infxrunb2 38525 climinff 38678 cncfshift 38759 cncficcgt0 38774 stoweidlem31 38924 stoweidlem34 38927 stoweidlem35 38928 stoweidlem51 38944 stoweidlem53 38946 stoweidlem54 38947 stoweidlem57 38950 stoweidlem59 38952 stoweidlem60 38953 fourierdlem31 39031 fourierdlem73 39072 iundjiun 39353 issmfle 39632 issmfgt 39643 issmfge 39656 cbvral2 39821 raaan2 39824 2reu3 39837 rspc2vd 41437 |
Copyright terms: Public domain | W3C validator |