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 1796 | . . 3 ⊢ Ⅎ𝑦⊤ | |
2 | nfral.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐴) |
4 | nfral.2 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
5 | 4 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝜑) |
6 | 1, 3, 5 | nfrald 3224 | . 2 ⊢ (⊤ → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑) |
7 | 6 | mptru 1535 | 1 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1529 Ⅎwnf 1775 Ⅎwnfc 2961 ∀wral 3138 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-13 2383 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 |
This theorem is referenced by: nfra2 3228 nfiing 4944 disjxun 5056 fiun 7635 f1iun 7636 opreu2reuALT 30168 bnj1228 32181 poimirlem26 34800 poimirlem27 34801 eliuniincex 41256 disjinfi 41334 limsupre3uzlem 41896 xlimmnfv 41995 xlimpnfv 41999 stoweidlem51 42217 stoweidlem53 42219 stoweidlem54 42220 stoweidlem57 42223 stoweidlem59 42225 stoweidlem60 42226 fourierdlem31 42304 fourierdlem73 42345 iundjiun 42623 meaiuninc3v 42647 issmfle 42903 issmfgt 42914 issmfge 42927 smfpimcc 42963 smfsup 42969 smfinf 42973 cbvral2 43182 2reu3 43190 2reu8i 43193 ichreuopeq 43482 reupr 43531 reuopreuprim 43535 |
Copyright terms: Public domain | W3C validator |