![]() |
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 1952 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | exbid.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | exbidh 1727 |
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 ax-5 1758 ax-6 1805 ax-7 1851 ax-12 1933 |
This theorem depends on definitions: df-bi 189 df-an 373 df-ex 1664 df-nf 1668 |
This theorem is referenced by: mobid 2318 rexbida 2896 rexeqf 2984 opabbid 4465 zfrepclf 4521 dfid3 4750 oprabbid 6344 axrepndlem1 9017 axrepndlem2 9018 axrepnd 9019 axpowndlem2 9023 axpowndlem3 9024 axpowndlem4 9025 axregnd 9029 axinfndlem1 9030 axinfnd 9031 axacndlem4 9035 axacndlem5 9036 axacnd 9037 opabdm 28219 opabrn 28220 pm14.122b 36774 pm14.123b 36777 |
Copyright terms: Public domain | W3C validator |