![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexanali | Structured version Visualization version Unicode version |
Description: A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.) (Proof shortened by Wolf Lammen, 27-Dec-2019.) |
Ref | Expression |
---|---|
rexanali |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfrex2 2838 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | iman 426 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | ralbii 2819 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | xchbinxr 313 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 |
This theorem depends on definitions: df-bi 189 df-an 373 df-ex 1664 df-ral 2742 df-rex 2743 |
This theorem is referenced by: nrexralim 2841 wfi 5413 qsqueeze 11494 ncoprmgcdne1b 14655 elcls 20089 ist1-2 20363 haust1 20368 t1sep 20386 bwth 20425 1stccnp 20477 filufint 20935 fclscf 21040 pmltpc 22401 ovolgelb 22433 itg2seq 22700 radcnvlt1 23373 pntlem3 24447 usgra2edg1 25110 archiabl 28515 ordtconlem1 28730 ceqsralv2 30358 frind 30481 limsucncmpi 31105 ftc1anclem5 32021 usgr2edg1 39292 usg2edgneu 39777 |
Copyright terms: Public domain | W3C validator |