New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > exbidv | Unicode version |
Description: Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
albidv.1 |
Ref | Expression |
---|---|
exbidv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1616 | . 2 | |
2 | albidv.1 | . 2 | |
3 | 1, 2 | exbidh 1591 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 176 wex 1541 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 |
This theorem depends on definitions: df-bi 177 df-ex 1542 |
This theorem is referenced by: 2exbidv 1628 3exbidv 1629 eubid 2211 eleq1 2413 eleq2 2414 rexbidv2 2637 ceqsex2 2895 alexeq 2968 ceqex 2969 sbc2or 3054 sbc5 3070 sbcex2 3095 sbcexg 3096 sbcabel 3123 eluni 3894 csbunig 3899 intab 3956 el1c 4139 opkelopkabg 4245 otkelins3kg 4254 opkelcokg 4261 opkelimagekg 4271 sfineq1 4526 sfineq2 4527 phiall 4618 cbvopab1 4632 cbvopab1s 4634 setconslem6 4736 csbxpg 4813 opeliunxp 4820 br1st 4858 br2nd 4859 brco 4883 dfdmf 4905 dfrnf 4962 csbrng 4966 dfco2a 5081 cores 5084 tz6.12-2 5346 fnrnfv 5364 dmfco 5381 funiunfv 5467 isomin 5496 cbvoprab1 5567 cbvoprab2 5568 oqelins4 5794 txpcofun 5803 erdmrn 5965 mapsn 6026 bren 6030 ce0nnul 6177 ce0ncpw1 6185 dflec3 6221 nclenc 6222 taddc 6229 |
Copyright terms: Public domain | W3C validator |