Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reubidv | Structured version Visualization version Unicode version |
Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 17-Oct-1996.) |
Ref | Expression |
---|---|
reubidv.1 |
Ref | Expression |
---|---|
reubidv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reubidv.1 | . . 3 | |
2 | 1 | adantr 481 | . 2 |
3 | 2 | reubidva 3125 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wcel 1990 wreu 2914 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-12 2047 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-nf 1710 df-eu 2474 df-reu 2919 |
This theorem is referenced by: reueqd 3148 sbcreu 3515 oawordeu 7635 xpf1o 8122 dfac2 8953 creur 11014 creui 11015 divalg 15126 divalg2 15128 lubfval 16978 lubeldm 16981 lubval 16984 glbfval 16991 glbeldm 16994 glbval 16997 joineu 17010 meeteu 17024 dfod2 17981 ustuqtop 22050 usgredg2vtxeuALT 26114 isfrgr 27122 frcond1 27130 frgr1v 27135 nfrgr2v 27136 frgr3v 27139 3vfriswmgr 27142 n4cyclfrgr 27155 eulplig 27337 riesz4 28923 cnlnadjeu 28937 poimirlem25 33434 poimirlem26 33435 hdmap1eulem 37113 hdmap1eulemOLDN 37114 hdmap14lem6 37165 |
Copyright terms: Public domain | W3C validator |