![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > exbid | Structured 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 1810 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | exbid.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | exbidh 1644 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-12 1794 |
This theorem depends on definitions: df-bi 185 df-ex 1588 df-nf 1591 |
This theorem is referenced by: mobid 2282 rexbida 2844 rexeqf 3012 opabbid 4454 zfrepclf 4509 dfid3 4737 oprabbid 6240 axrepndlem1 8859 axrepndlem2 8860 axrepnd 8861 axpowndlem2 8865 axpowndlem2OLD 8866 axpowndlem3 8867 axpowndlem3OLD 8868 axpowndlem4 8869 axregnd 8873 axregndOLD 8874 axinfndlem1 8875 axinfnd 8876 axacndlem4 8880 axacndlem5 8881 axacnd 8882 opabdm 26079 opabrn 26080 fpwrelmapffslem 26168 pm14.122b 29817 pm14.123b 29820 |
Copyright terms: Public domain | W3C validator |