![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > exbid | Structured version Visualization version Unicode version |
Description: Formula-building rule for existential quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.) |
Ref | Expression |
---|---|
exbid.1 |
![]() ![]() ![]() ![]() |
exbid.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
exbid |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exbid.1 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 1 | nfri 1972 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | exbid.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | exbidh 1735 |
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 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-12 1950 |
This theorem depends on definitions: df-bi 190 df-ex 1672 df-nf 1676 |
This theorem is referenced by: mobid 2338 rexbida 2887 rexeqf 2970 opabbid 4458 zfrepclf 4514 dfid3 4755 oprabbid 6363 axrepndlem1 9035 axrepndlem2 9036 axrepnd 9037 axpowndlem2 9041 axpowndlem3 9042 axpowndlem4 9043 axregnd 9047 axinfndlem1 9048 axinfnd 9049 axacndlem4 9053 axacndlem5 9054 axacnd 9055 opabdm 28295 opabrn 28296 pm14.122b 36844 pm14.123b 36847 |
Copyright terms: Public domain | W3C validator |