Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfralxy | GIF version |
Description: Old name for nfralw 2507. (Contributed by Jim Kingdon, 30-May-2018.) (New usage is discouraged.) |
Ref | Expression |
---|---|
nfralxy.1 | ⊢ Ⅎ𝑥𝐴 |
nfralxy.2 | ⊢ Ⅎ𝑥𝜑 |
Ref | Expression |
---|---|
nfralxy | ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nftru 1459 | . . 3 ⊢ Ⅎ𝑦⊤ | |
2 | nfralxy.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | a1i 9 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐴) |
4 | nfralxy.2 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
5 | 4 | a1i 9 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝜑) |
6 | 1, 3, 5 | nfraldxy 2503 | . 2 ⊢ (⊤ → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑) |
7 | 6 | mptru 1357 | 1 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑 |
Colors of variables: wff set class |
Syntax hints: ⊤wtru 1349 Ⅎwnf 1453 Ⅎwnfc 2299 ∀wral 2448 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-4 1503 ax-17 1519 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-tru 1351 df-nf 1454 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ral 2453 |
This theorem is referenced by: nfra2xy 2512 rspc2 2845 sbcralt 3031 sbcralg 3033 raaanlem 3520 nfint 3841 nfiinxy 3900 nfpo 4286 nfso 4287 nfse 4326 nffrfor 4333 nfwe 4340 ralxpf 4757 funimaexglem 5281 fun11iun 5463 dff13f 5749 nfiso 5785 mpoeq123 5912 nfofr 6067 fmpox 6179 nfrecs 6286 xpf1o 6822 ac6sfi 6876 ismkvnex 7131 lble 8863 fzrevral 10061 nfsum1 11319 nfsum 11320 fsum2dlemstep 11397 fisumcom2 11401 nfcprod1 11517 nfcprod 11518 bezoutlemmain 11953 cnmpt21 13085 setindis 14002 bdsetindis 14004 strcollnfALT 14021 isomninnlem 14062 iswomninnlem 14081 ismkvnnlem 14084 |
Copyright terms: Public domain | W3C validator |