Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ralbiia | Structured version Visualization version Unicode version |
Description: Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.) |
Ref | Expression |
---|---|
ralbiia.1 |
Ref | Expression |
---|---|
ralbiia |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralbiia.1 | . . 3 | |
2 | 1 | pm5.74i 260 | . 2 |
3 | 2 | ralbii2 2978 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wcel 1990 wral 2912 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 |
This theorem depends on definitions: df-bi 197 df-ral 2917 |
This theorem is referenced by: poinxp 5182 soinxp 5183 seinxp 5185 dffun8 5916 funcnv3 5959 fncnv 5962 fnres 6007 fvreseq0 6317 isoini2 6589 smores 7449 tfr3ALT 7498 resixp 7943 ixpfi2 8264 marypha1lem 8339 ac5num 8859 acni2 8869 acndom 8874 dfac4 8945 brdom7disj 9353 brdom6disj 9354 fpwwe2lem8 9459 axgroth6 9650 rabssnn0fi 12785 lo1res 14290 isprm5 15419 prmreclem2 15621 tsrss 17223 gass 17734 efgval2 18137 efgsres 18151 isdomn2 19299 islinds2 20152 isclo 20891 ptclsg 21418 ufilcmp 21836 cfilres 23094 ovolgelb 23248 volsup2 23373 vitali 23382 itg1climres 23481 itg2seq 23509 itg2monolem1 23517 itg2mono 23520 itg2i1fseq 23522 itg2cn 23530 ellimc2 23641 rolle 23753 lhop1 23777 itgsubstlem 23811 tdeglem4 23820 dvdsmulf1o 24920 dchrelbas2 24962 selbergsb 25264 axcontlem2 25845 dfconngr1 27048 hodsi 28634 ho01i 28687 ho02i 28688 lnopeqi 28867 nmcopexi 28886 nmcfnexi 28910 cnlnadjlem3 28928 cnlnadjlem5 28930 leop3 28984 pjssposi 29031 largei 29126 mdsl2i 29181 mdsl2bi 29182 elat2 29199 dmdbr5ati 29281 cdj3lem3b 29299 subfacp1lem3 31164 dfso3 31601 phpreu 33393 ptrecube 33409 mblfinlem1 33446 voliunnfl 33453 acsfn1p 37769 ntrneiel2 38384 ismbl3 40203 ismbl4 40210 sge0lefimpt 40640 sbgoldbalt 41669 |
Copyright terms: Public domain | W3C validator |