![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexeqbidv | Structured version Visualization version Unicode version |
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) |
Ref | Expression |
---|---|
raleqbidv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
raleqbidv.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
rexeqbidv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | raleqbidv.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | rexeqdv 3006 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | raleqbidv.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | rexbidv 2913 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | bitrd 261 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-cleq 2455 df-clel 2458 df-nfc 2592 df-rex 2755 |
This theorem is referenced by: supeq123d 7990 fpwwe2lem13 9093 hashge2el2difr 12671 vdwpc 14979 ramval 15009 ramvalOLD 15010 mreexexlemd 15599 iscat 15627 iscatd 15628 catidex 15629 gsumval2a 16571 ismnddef 16587 ismndOLD 16591 mndpropd 16611 isgrp 16726 isgrpd2e 16737 cayleyth 17105 psgnfval 17190 iscyg 17563 ltbval 18744 opsrval 18747 scmatval 19578 pmatcollpw3fi1lem2 19860 pmatcollpw3fi1 19861 neiptopnei 20197 is1stc 20505 2ndc1stc 20515 2ndcsep 20523 islly 20532 isnlly 20533 ucnval 21341 imasdsf1olem 21437 met2ndc 21587 evthicc 22459 istrkgld 24556 legval 24678 ishpg 24850 iscgra 24900 isinag 24928 isleag 24932 nb3graprlem2 25229 erclwwlkeq 25588 2wlksot 25644 2spthsot 25645 isplig 25958 isgrp2d 26012 isgrpda 26074 isexid 26094 isrngo 26155 isrngod 26156 nmoofval 26452 istrkg2d 29532 iscvm 30031 cvmlift2lem13 30087 br8 30445 br6 30446 br4 30447 brsegle 30924 hilbert1.1 30970 poimirlem26 32011 poimirlem28 32013 poimirlem29 32014 cover2g 32086 lshpset 32589 cvrfval 32879 isatl 32910 ishlat1 32963 llnset 33115 lplnset 33139 lvolset 33182 lineset 33348 lcfl7N 35114 lcfrlem8 35162 lcfrlem9 35163 lcf1o 35164 hvmapffval 35371 hvmapfval 35372 hvmapval 35373 mzpcompact2lem 35638 eldioph 35645 aomclem8 35964 ovnval 38400 nnsum3primes4 38921 nnsum3primesprm 38923 nnsum3primesgbe 38925 wtgoldbnnsum4prm 38935 bgoldbnnsum3prm 38937 nbgrval 39456 nb3grprlem2 39505 zlidlring 40201 uzlidlring 40202 lcoop 40477 ldepsnlinc 40574 nnpw2p 40670 |
Copyright terms: Public domain | W3C validator |